Document Open Access Logo

Timed Basic Parallel Processes

Authors Lorenzo Clemente , Piotr Hofman , Patrick Totzke

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.15.pdf
  • Filesize: 0.74 MB
  • 16 pages

Document Identifiers

Author Details

Lorenzo Clemente
  • University of Warsaw, Poland
Piotr Hofman
  • University of Warsaw, Poland
Patrick Totzke
  • University of Liverpool, UK

Funding

  • Clemente, Lorenzo: Partially supported by Polish NCN grant 2017/26/D/ST6/00201.
  • Hofman, Piotr: Partially supported by Polish NCN grant 2016/21/D/ST6/01368.

Acknowledgements

Many thanks to Rasmus Ibsen-Jensen for helpful discussions and pointing us towards [Hansen et al., 2013].

Cite AsGet BibTex

Lorenzo Clemente, Piotr Hofman, and Patrick Totzke. Timed Basic Parallel Processes. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.15

Abstract

Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such may be used to model networks of independent timed automata with process creation. We show that the coverability and reachability problems (with unary encoded target multiplicities) are PSPACE-complete and EXPTIME-complete, respectively. For the special case of 1-clock TBPP, both are NP-complete and hence not more complex than for untimed BPP. This contrasts with known super-Ackermannian-completeness and undecidability results for general timed Petri nets. As a result of independent interest, and basis for our NP upper bounds, we show that the reachability relation of 1-clock TA can be expressed by a formula of polynomial size in the existential fragment of linear arithmetic, which improves on recent results from the literature.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
Keywords
  • Timed Automata
  • Petri Nets

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. P. A. Abdulla, M. F. Atig, and J. Cederberg. Timed Lossy Channel Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2012. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2012.374.
  2. P. A. Abdulla, M. F. Atig, and J. Stenman. Dense-Timed Pushdown Automata. In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2012. URL: https://doi.org/10.1109/LICS.2012.15.
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke. Universal Safety for Timed Petri Nets is PSPACE-complete. In International Conference on Concurrency Theory (CONCUR), 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.6.
  4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Shankara Narayanan Krishna. Perfect Timed Communication Is Hard. In International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2018. Google Scholar
  5. Parosh Aziz Abdulla and Bengt Jonsson. Model checking of systems with many identical timed processes. Theoretical Computer Science, 2003. URL: https://doi.org/10.1016/S0304-3975(01)00330-9.
  6. Parosh Aziz Abdulla and Aletta Nylén. Timed Petri Nets and BQOs. In Applications and Theory of Petri Nets and Concurrency (PETRI NETS), 2001. Google Scholar
  7. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  8. M. Benerecetti, S. Minopoli, and A. Peron. Analysis of Timed Recursive State Machines. In International Symposium on Temporal Representation and Reasoning (TIME), 2010. URL: https://doi.org/10.1109/TIME.2010.10.
  9. Massimo Benerecetti and Adriano Peron. Timed recursive state machines: Expressiveness and complexity. Theoretical Computer Science, 2016. URL: https://doi.org/10.1016/j.tcs.2016.02.021.
  10. Beatrice Bérard, Anne Labroue, and Philippe Schnoebelen. Verifying Performance Equivalence for Timed Basic Parallel Processes. In International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), 2000. Google Scholar
  11. Bernard Boigelot, Sébastien Jodogne, and Pierre Wolper. An Effective Decision Procedure for Linear Arithmetic over the Integers and Reals. ACM Trans. Comput. Logic, 2005. URL: https://doi.org/10.1145/1071596.1071601.
  12. Ahmed Bouajjani, Rachid Echahed, and Riadh Robbana. On the Automatic Verification of Systems with Continuous Variables and Unbounded Discrete Data Structures. In Hybrid Systems (HS), 1994. Google Scholar
  13. Patricia Bouyer, Kim G. Larsen, Nicolas Markey, and Jacob Illum Rasmussen. Almost Optimal Strategies in One Clock Priced Timed Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2006. Google Scholar
  14. Søren Christensen. Decidability and Decomposition in Process Algebras. PhD thesis, School of Informatics, University of Edinburgh, 1993. Google Scholar
  15. Lorenzo Clemente. Decidability of Timed Communicating Automata. arXiv e-prints, 2018. URL: http://arxiv.org/abs/1804.07815.
  16. Lorenzo Clemente, Frédéric Herbreteau, Amelie Stainer, and Grégoire Sutre. Reachability of Communicating Timed Processes. In International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), 2013. URL: https://doi.org/10.1007/978-3-642-37075-5_6.
  17. Lorenzo Clemente, Piotr Hofman, and Patrick Totzke. Timed Basic Parallel Processes. arXiv e-prints, July 2019. URL: http://arxiv.org/abs/1907.01240.
  18. Lorenzo Clemente and Sławomir Lasota. Binary reachability of timed pushdown automata via quantifier elimination. In International Colloquium on Automata, Languages and Programming (ICALP), 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.118.
  19. Lorenzo Clemente, Sławomir Lasota, Ranko Lazić, and Filip Mazowiecki. Timed pushdown automata and branching vector addition systems. In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2017. Google Scholar
  20. Hubert Comon and Yan Jurski. Timed Automata and the Theory of Real Numbers. In International Conference on Concurrency Theory (CONCUR), 1999. Google Scholar
  21. Zhe Dang. Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks. In Computer Aided Verification (CAV), 2001. Google Scholar
  22. C. Dima. Computing reachability relations in timed automata. In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2002. URL: https://doi.org/10.1109/LICS.2002.1029827.
  23. Catalin Dima. A Class of Automata for Computing Reachability Relations in Timed Systems. In Verification of Infinite State Systems with Applications to Security (VISSAS), 2005. Google Scholar
  24. Javier Esparza. Petri Nets, Commutative Context-Free Grammars, and Basic Parallel Processes. Fundamenta Informaticae, 1997. Google Scholar
  25. John Fearnley and Marcin Jurdziński. Reachability in two-clock timed automata is PSPACE-complete. Information and Computation, 2015. URL: https://doi.org/10.1016/j.ic.2014.12.004.
  26. Jeanne Ferrante and Charles Rackoff. A Decision Procedure for the First Order Theory of Real Addition with Order. SIAM Journal on Computing, 1975. Google Scholar
  27. Martin Fränzle, Karin Quaas, Mahsa Shirmohammadi, and James Worrell. Effective Definability of the Reachability Relation in Timed Automata. arXiv e-prints, 2019. URL: http://arxiv.org/abs/1903.09773.
  28. Serge Haddad, Sylvain Schmitz, and Philippe Schnoebelen. The Ordinal Recursive Complexity of Timed-Arc Petri Nets, Data Nets, and Other Enriched Nets. In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2012. URL: https://doi.org/10.1109/LICS.2012.46.
  29. Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Peter Bro Miltersen. A Faster Algorithm for Solving One-Clock Priced Timed Games. In International Conference on Concurrency Theory (CONCUR), 2013. Google Scholar
  30. Marcin Jurdziński and Ashutosh Trivedi. Reachability-time Games on Timed Automata. In International Colloquium on Automata, Languages and Programming (ICALP), 2007. Google Scholar
  31. Pavel Krčál and Radek Pelánek. On Sampled Semantics of Timed Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2005. Google Scholar
  32. Pavel Krcal and Wang Yi. Communicating timed automata: the more synchronous, the more difficult to verify. In Computer Aided Verification (CAV), 2006. URL: https://doi.org/10.1007/11817963_24.
  33. F. Laroussinie, N. Markey, and Ph. Schnoebelen. Model Checking Timed Automata with One or Two Clocks. In International Conference on Concurrency Theory (CONCUR), 2004. Google Scholar
  34. Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer (STTT), 1997. URL: https://doi.org/10.1007/s100090050010.
  35. Slawomir Lasota and Igor Walukiewicz. Alternating timed automata. ACM Trans. Comput. Logic, 2008. URL: https://doi.org/10.1145/1342991.1342994.
  36. Philip Meir Merlin. A Study of the Recoverability of Computing Systems. PhD thesis, University of California, Irvine, 1974. Google Scholar
  37. J. Ouaknine and J. Worrell. On the decidability of metric temporal logic. In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2005. URL: https://doi.org/10.1109/LICS.2005.33.
  38. Louchka Popova. On Time Petri Nets. Journal of Information Processing and Cybernetics, 1991. Google Scholar
  39. Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus Premier Congrès des Mathématicienes des Pays Slaves, 1930. Google Scholar
  40. Karin Quaas. Verification for Timed Automata extended with Unbounded Discrete Data Structures. Logical Methods in Computer Science, 2015. URL: https://doi.org/10.2168/LMCS-11(3:20)2015.
  41. Valentin Valero Ruiz, Fernando Cuartero Gomez, and David de Frutos Escrig. On Non-Decidability of Reachability for Timed-Arc Petri Nets. In International Workshop on Petri Nets and Performance Models (PNPM), 1999. Google Scholar
  42. Ashutosh Trivedi. Competative Optimisation on Timed Automata. PhD thesis, University of Warwick, 2009. Google Scholar
  43. Ashutosh Trivedi and Dominik Wojtczak. Recursive Timed Automata. In International Symposium on Automated Technology for Verification and Analysis (ATVA), 2010. Google Scholar
  44. Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. On the Complexity of Equational Horn Clauses. In International Conference on Automated Deduction (CADE), 2005. URL: https://doi.org/10.1007/11532231_25.
  45. Volker Weispfenning. Mixed Real-integer Linear Quantifier Elimination. In International Symposium on Symbolic and Algebraic Computation (ISSAC), 1999. URL: https://doi.org/10.1145/309831.309888.
  46. Sergio Yovine. KRONOS: a verification tool for real-time systems. International Journal on Software Tools for Technology Transfer, 1997. URL: https://doi.org/10.1007/s100090050009.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact