Interrupt Timed Automata with Auxiliary Clocks and Parameters

• Autorzy: Bérard B. , Jovanović A. , Haddad S. , Lime D.

Identyfikatory

DOI

10.3233/FI-2016-1313

• Języki publikacji: EN

Abstrakty

EN

Interrupt Timed Automata (ITA) are an expressive timed model, introduced to take into account interruptions according to levels. Due to this feature, this formalism is incomparable with Timed Automata. However several decidability results related to reachability and model checking have been obtained. We add auxiliary clocks to ITA, thereby extending its expressive power while preserving decidability of reachability. Moreover, we define a parametrized version of ITA, with polynomials of parameters appearing in guards and updates. While parametric reasoning is particularly relevant for timed models, it very often leads to undecidability results. We prove that various reachability problems, including robust reachability, are decidable for this model, and we give complexity upper bounds for a fixed or variable number of clocks, levels and parameters.

Słowa kluczowe

EN

machine theory; parameter estimation; problem solving; robust control; mathematical models

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 143, nr 3/4
• Strony: 235--259
• Opis fizyczny: Bibliogr. 24 poz., rys.

Twórcy

autor

Bérard B.

• Sorbonne Université UPMC-Paris 6, CNRS UMR 7606 Paris, France

autor

Jovanović A.

• Department of Computer Science, University of Oxford, Oxford, UK

autor

Haddad S.

• ENS Cachan, LSV, CNRS, INRIA Cachan, France

autor

Lime D.

• École Centrale de Nantes, IRCCyN, CNRS Nantes, France

Bibliografia

• [1] Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH, Nicollin X, et al. The algorithmic analysis of hybrid systems. Theoretical Computer Science. 1995;138(1):3–34. doi:10.1016/0304-3975(94)00202-T.
• [2] Alur R, Dill DL. Automata for modeling real-time systems. In: ICALP’90. Springer; 1990. p. 322–335. doi:10.1007/BFb0032042.
• [3] Bérard B, Haddad S. Interrupt Timed Automata. In: FoSSaCS’09. vol. 5504 of LNCS. Springer; 2009. p. 197–211. doi:10.1007/978-3-642-00596-1 15.
• [4] Bérard B, Haddad S, Sassolas M. Interrupt Timed Automata: Verification and Expressiveness. Formal Methods in System Design. 2012;40(1):41–87. doi:10.1007/s10703-011-0140-2.
• [5] Alur R, Henzinger TA, Vardi MY. Parametric real-time reasoning. In: ACM Symp. on Theory of Computing. ACM; 1993. p. 592–601. Available from: DBLP,http://dblp.uni-trier.de.
• [6] Miller JS. Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata. In: HSCC’00. vol. 1790 of LNCS. Springer; 2000. p. 296–309. DBLP, http://dblp.uni-trier.de.
• [7] Doyen L. Robust Parametric Reachability for Timed Automata. Information Processing Letters. 2007; 102(5):208–213. doi:10.1016/j.ipl.2006.11.018.
• [8] Bérard B, Fribourg L. Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol. In: CAV’99. vol. 1633 of LNCS. Springer; 1999. p. 96–107.
• [9] André É, Chatain Th, Encrenaz E, Fribourg L. An Inverse Method for Parametric Timed Automata. Int J of Foundations of Comp Sci. 2009;20(5):819–836.
• [10] André É, Fribourg L, K¨uhne U, Soulat R. IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems. In: FM’12. vol. 7436 of LNCS. Springer; 2012. p. 33–36. doi:10.1007/978-3-642-32759-9 6.
• [11] Jovanović A, Lime D, Roux OH. Integer Parameter Synthesis for Real-Time Systems. IEEE Transactions on Software Engineering (TSE). 2015;41(5):445–461. doi:10.1109/TSE.2014.2357445.
• [12] Traonouez LM, Lime D, Roux OH. Parametric Model-Checking of Stopwatch Petri Nets. Journal of Universal Computer Science (JUCS). 2009;15(17):3273–3304. doi:10.1007/978-3-642-00768-2 6.
• [13] Lime D, Roux OH, Seidner C, Traonouez LM. Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In: TACAS’09. vol. 5505 of LNCS. Springer; 2009. p. 54–57. doi:10.1007/978-3-642-00768-2 6.
• [14] Alur R, Henzinger TA, Ho PH. Automatic Symbolic Verification of Embedded Systems. IEEE Transactions on Software Engineering. 1996; 22(3):181–201. doi:10.1109/32.489079.
• [15] Henzinger TA, Ho PH, Wong-Toi H. HyTech: A Model-Checker for Hybrid Systems. Software Tools for Technology Transfer. 1997;1:110–122.
• [16] Hune T, Romijn J, Stoelinga M, Vaandrager F. Linear Parametric Model Checking of Timed Automata. J of Logic and Alg Prog. 2002;52-53:183–220. doi:10.1016/S1567-8326(02)00037-1.
• [17] Bozzelli L, La Torre S. Decision problems for lower/upper bound parametric timed automata. Formal Methods in System Design. 2009;35(2):121–151. doi:10.1007/s10703-009-0074-0.
• [18] Bundala D, Ouaknine J. Advances in Parametric Real-Time Reasoning. In: MFCS’14. vol. 8634 of LNCS. Springer; 2014. p. 123–134. doi:10.1007/978-3-662-44522-8 11.
• [19] Bruyère V, Dall’Olio E, Raskin J. Durations and parametric model-checking in timed automata. ACM Trans Comput Log. 2008;9(2). doi:10.1007/3-540-36494-3 60.
• [20] Bylander T. The Computational Complexity of Propositional STRIPS Planning. Artificial Intelligence. 1994;69(1-2):165–204. doi:10.1016/0004-3702(94)90081-7.
• [21] Zaslavsky T. Facing up to Arrangements: Face-Count Formulas for Partitions of Space by Hyperplanes. AMS Memoirs. 1975;1(154). doi:http://dx.doi.org/10.1090/memo/0154.
• [22] Roos C, Terlaky T, Vial JP. Theory and Algorithms for Linear Optimization. An Interior Point Approach. Wiley-Interscience, John Wiley & Sons Ltd; 1997. ISBN: 0471956767, 9780471956761.
• [23] Courcoubetis C, Yannakakis M. Minimum and Maximum Delay Problems in Real-Time Systems. Formal Methods in System Design. 1992;1(4):385–415. doi:10.1007/BF00709157.
• [24] Canny JF. Some Algebraic and Geometric Computations in PSPACE. In: ACM Symp. on Theory of Computing. ACM; 1988. p. 460–467. Available from: http://www.eecs.berkeley.edu/Pubs/TechRpts/1988/6041.html.