Real-Time Model-Checking: Parameters everywhere

Veronique Bruyere; Jean-Francois Raskin

doi:10.2168/LMCS-3(1:7)2007

Veronique Bruyere ; Jean-Francois Raskin - Real-Time Model-Checking: Parameters everywhere

lmcs:2229 - Logical Methods in Computer Science, February 27, 2007, Volume 3, Issue 1 - https://doi.org/10.2168/LMCS-3(1:7)2007

Real-Time Model-Checking: Parameters everywhereArticle

Authors: Veronique Bruyere ; Jean-Francois Raskin

In this paper, we study the model-checking and parameter synthesis problems of the logic TCTL over discrete-timed automata where parameters are allowed both in the model (timed automaton) and in the property (temporal formula). Our results are as follows. On the negative side, we show that the model-checking problem of TCTL extended with parameters is undecidable over discrete-timed automata with only one parametric clock. The undecidability result needs equality in the logic. On the positive side, we show that the model-checking and the parameter synthesis problems become decidable for a fragment of the logic where equality is not allowed. Our method is based on automata theoretic principles and an extension of our method to express durations of runs in timed automata using Presburger arithmetic.

https://doi.org/10.2168/LMCS-3(1:7)2007

Source: arXiv.org:cs/0701138

Volume: Volume 3, Issue 1

Published on: February 27, 2007

Submitted on: July 19, 2005

Keywords: Computer Science - Logic in Computer Science,F.1.1

Licence: arXiv.org - Assumed non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

21 Documents citing this article

Étienne André;Didier Lime;Dylan Marinho;Jun Sun, 2022, Guaranteeing Timed Opacity using Parametric Timed Model Checking, 31, 4, pp. 1-36, 10.1145/3502851, https://hal.science/hal-03798157.

Aleksandra Jovanović;Didier Lime;Olivier Henri Roux, 2018, A game approach to the parametric control of real-time systems, International Journal of Control, 92, 9, pp. 2025-2036, 10.1080/00207179.2018.1426883, https://hal.science/hal-02010912/file/jovanovic-IJC-18.pdf.

Aleksandra Jovanović;Marta Kwiatkowska, 2017, Parameter synthesis for probabilistic timed automata using stochastic game abstractions, Theoretical Computer Science, 735, pp. 64-81, 10.1016/j.tcs.2017.05.005, https://doi.org/10.1016/j.tcs.2017.05.005.

Étienne André, 2017, What’s decidable about parametric timed automata?, arXiv (Cornell University), 21, 2, pp. 203-219, 10.1007/s10009-017-0467-0, https://arxiv.org/abs/1907.01721.

Naima Jbeli;Zohra Sbaï;Rahma Ben Ayed, Lecture notes in computer science, On Expressiveness of TCTL $$^{\varDelta }_{h}$$ for Model Checking Distributed Systems, pp. 323-332, 2016, 10.1007/978-3-319-45243-2_30.

Étienne André, arXiv (Cornell University), What’s Decidable About Parametric Timed Automata?, pp. 52-68, 2016, 10.1007/978-3-319-29510-7_3, https://arxiv.org/abs/1907.01721.

Étienne André;Thomas Chatain;César Rodríguez, 2016, Preserving Partial-Order Runs in Parametric Time Petri Nets, 16, 2, pp. 1-26, 10.1145/3012283, https://hal.inria.fr/hal-01425696.

Etienne Andre;Thomas Chatain;Cesar Rodriguez, Preserving Partial Order Runs in Parametric Time Petri Nets, 11, pp. 120-129, 2015, Brussels, Belgium, 10.1109/acsd.2015.20, https://hal.inria.fr/hal-01425696.

Étienne André;Didier Lime;Olivier H. Roux, Integer-Complete Synthesis for Bounded Parametric Timed Automata, pp. 7-19, 2015, 10.1007/978-3-319-24537-9_2, https://hal.science/hal-02939637.

Aleksandra Jovanovic;Didier Lime;Olivier H. Roux, 2014, Integer Parameter Synthesis for Real-Time Systems, IEEE Transactions on Software Engineering, 41, 5, pp. 445-461, 10.1109/tse.2014.2357445, https://hal.archives-ouvertes.fr/hal-02939617/file/jovanovic-TSE-15.pdf.

Barbara Di Giampaolo;Salvatore La Torre;Margherita Napoli, 2014, Parametric metric interval temporal logic, Theoretical Computer Science, 564, pp. 131-148, 10.1016/j.tcs.2014.11.019, https://doi.org/10.1016/j.tcs.2014.11.019.

Hassan Motallebi;Mohammad Abdollahi Azgomi, 2014, Parametric multisingular hybrid Petri nets: Formal definitions and analysis techniques, Information and Computation, 241, pp. 321-348, 10.1016/j.ic.2014.11.001.

Aleksandra Jovanović;Didier Lime;Olivier H. Roux, Lecture notes in computer science, Integer Parameter Synthesis for Timed Automata, pp. 401-415, 2013, 10.1007/978-3-642-36742-7_28.

Aleksandra Jovanović;Didier Lime;Olivier H. Roux, Lecture notes in computer science, Synthesis of Bounded Integer Parameters for Parametric Timed Reachability Games, pp. 87-101, 2013, 10.1007/978-3-319-02444-8_8.

Etienne Andre, CiteSeer X (The Pennsylvania State University), Observer Patterns for Real-Time Systems, pp. 125-134, 2013, Singapore, Singapore, 10.1109/iceccs.2013.26, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.648.3939.

Karen Godary-Dejean;David Andreu, 2013, Formal Validation of a Deterministic MAC Protocol, 12, 1, pp. 1-23, 10.1145/2406336.2406342, https://hal-lirmm.ccsd.cnrs.fr/lirmm-00679892v2/file/TECS_tmp.pdf.

Md Tawhid Bin Waez;Juergen Dingel;Karen Rudie, 2013, A survey of timed automata for the development of real-time systems, Computer Science Review, 9, pp. 1-26, 10.1016/j.cosrev.2013.05.001.

André Platzer, Springer eBooks, Introduction, pp. 1-29, 2010, 10.1007/978-3-642-14509-4_1.

Barbara Di Giampaolo;Salvatore La Torre;Margherita Napoli, Lecture notes in computer science, Parametric Metric Interval Temporal Logic, pp. 249-260, 2010, 10.1007/978-3-642-13089-2_21.

Louis-Marie Traonouez;Didier Lime;Olivier H. Roux, Lecture notes in computer science, Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph, pp. 280-294, 2008, 10.1007/978-3-540-85778-5_20.

Najla Chamseddine;Marie Duflot;Laurent Fribourg;Claudine Picaronny;Jeremy Sproston, CiteSeer X (The Pennsylvania State University), Computing Expected Absorption Times for Parametric Determinate Probabilistic Timed Automata, pp. 254-263, 2008, St Malo, France, 10.1109/qest.2008.34, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.220.46.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1518 times.

This article's PDF has been downloaded 478 times.