Skip to Main content Skip to Navigation
Conference papers

Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP

Iulian Ober 1
1 IRIT-ARGOS - Advancing Rigorous Software and System Engineering
IRIT - Institut de recherche en informatique de Toulouse
Abstract : 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.
Complete list of metadatas

Cited literature [28 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-02279416
Contributor : Open Archive Toulouse Archive Ouverte (oatao) <>
Submitted on : Thursday, September 5, 2019 - 11:45:45 AM
Last modification on : Tuesday, September 8, 2020 - 10:40:05 AM
Long-term archiving on: : Thursday, February 6, 2020 - 5:39:23 AM

File

ober_22531.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02279416, version 1
  • OATAO : 22531

Citation

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⟩

Share

Metrics

Record views

79

Files downloads

198