Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP

Iulian Ober (1, 2)

1 IRIT-ARGOS - Advancing Rigorous Software and System Engineering
2 UT2J - Université Toulouse - Jean Jaurès

We study the reduction of bounded reachability analysis of timed automata (TA) to a Mixed Integer Linear Programming (MILP) problem. While bounded model checking of timed automata has been explored in the literature based on the satisfiability of Boolean constraint formulas over linear arithmetic constraints verified using SAT Modulo Theory (SMT) solvers, the approach presented in this paper opens up the alternative of using MILP solvers. We present some preliminary results comparing the two approaches and provide ideas on how linear optimization can be useful for analyzing the behavior of TA. The results are supported by a prototype implementation which relies either on a MILP solver (Gurobi) or an SMT solver (MathSAT). Certain techniques for reducing the search space and improving the performance are also discussed.

Mots clés: MILP; Mixed Integer Linear Programming

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués; Cryptographie et sécurité [cs.CR]; Interface homme-machine [cs.HC]; Architectures Matérielles [cs.AR]; Modélisation et simulation

Iulian Ober. Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP. 23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS 2018), Sep 2018, Maynoooth, Ireland. pp.269-283. ⟨hal-02279416⟩