Theory and Applications of Reachability Analysis in the Discrete Space

• Applicant: Professor Dr. Amr Alanwar
• Subject Area: Automation, Mechatronics, Control Systems, Intelligent Technical Systems, Robotics
• Term: since 2025
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 564740977

Reachability analysis is a vital tool in control systems for formally verifying logical system behavior and preventing undesired states. However, when dealing with logical systems over Boolean vector spaces, the computational complexity grows exponentially with the dimension, posing a significant challenge. This "curse of dimensionality" necessitates innovative approaches to mitigate complexities. Inspired by the effectiveness of set-based theory in real vector spaces, this proposal introduces novel applications of my previously proposed binary set representations - logical zonotopes and polynomial logical zonotopes - which are constructed by XORing a binary vector with a combination of other binary vectors called generators. An approach is developed for the formal verification of logical systems to deal with uncertain inputs using binary sets. This involves leveraging logical zonotopes and polynomial logical zonotopes, capable of representing up to 2^n points with just n generators, enabling efficient logical operations in the generator space, and streamlining reachability analysis. Instead of verifying single inputs, the proposed methodologies ensure correctness and safety by computing reachable sets of system outputs, leveraging binary sets. Furthermore, A strategy within the generator space of binary sets is proposed, which enhances model-checking efficiency against linear temporal logic specifications. Additionally, the application of binary set representations extends to the search for encryption keys to detect insecure encryption schemes, transforming it into a forward model-based reachability analysis problem with the uncertain bit key, which contains 0 and 1 in a set. By leveraging set theory to represent sets of uncertain bits, this approach significantly improves the efficiency of exhaustive key searches by concurrently exploring both 0 and 1 key values for each bit. Considering messages and their ciphertexts, the goal is to execute encryption using sets of keys, resulting in a corresponding set of ciphertexts. If the given ciphertext does not belong to the set of ciphers, I can confidently eliminate the set of keys from my exhaustive search. Otherwise, I can divide this key set into smaller subsets and continue the search until I find the secret key. Overall, this proposal aims to underscore reachability analysis as a potent methodology applicable to diverse problems, including digital verification, model checking, and exhaustive key searches.

• DFG Programme: Emmy Noether Independent Junior Research Groups
• International Connection: Sweden
• Cooperation Partner: Professor Karl Henrik Johansson, Ph.D.