OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP

Ober, Iulian Sorin Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP. (2018) In: 23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS 2018), 3 September 2018 - 5 September 2018 (Maynoooth, Ireland).

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
668kB

Official URL: https://doi.org/10.1007/978-3-030-00244-2_18

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.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in Volume 11119 of Lecture Notes in Computer Science ISSN : 0302-9743 ISBN 978-3-030-00243-5 The original PDF is available at: https://link.springer.com/chapter/10.1007/978-3-030-00244-2_18
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:21 Jun 2019 12:18

Repository Staff Only: item control page