Document Open Access Logo

A Uniform Framework for Timed Automata

Authors Tomasz Brengos, Marco Peressotti

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.26.pdf
  • Filesize: 0.52 MB
  • 15 pages

Document Identifiers

Author Details

Tomasz Brengos
Marco Peressotti

Cite AsGet BibTex

Tomasz Brengos and Marco Peressotti. A Uniform Framework for Timed Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 26:1-26:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.26

Abstract

Timed automata, and machines alike, currently lack a general mathematical characterisation. In this paper we provide a uniform coalgebraic understanding of these devices. This framework encompasses known behavioural equivalences for timed automata and paves the way for the extension of these notions to new timed behaviours and for the instantiation of established results from the coalgebraic theory as well. Key to this work is the use of lax functors for they allow us to model time flow as a context property and hence offer a general and expressive setting where to study timed systems: the index category encodes "how step sequences form executions" (e.g. whether steps duration get accumulated or kept distinct) whereas the base category encodes "step nature and composition" (e.g. non-determinism and labels). Finally, we develop the notion of general saturation for lax functors and show how equivalences of interest for timed behaviours are instances of this notion. This characterisation allows us to reason about the expressiveness of said notions within a uniform framework and organise them in a spectrum independent from the behavioural aspects encoded in the base category.
Keywords
  • coalgebras
  • lax functors
  • general saturation
  • timed behavioural equivalence
  • timed language equivalence

Metrics

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

References

  1. Peter Aczel and Nax Mendler. A final coalgebra theorem. In D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, and A. Poigné, editors, Proc. CTCS, volume 389 of Lecture Notes in Computer Science, pages 357-365. Springer, 1989. Google Scholar
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, April 1994. Google Scholar
  3. Filippo Bonchi, Marcello M. Bonsangue, Helle Hvid Hansen, Prakash Panangaden, Jan J. M. M. Rutten, and Alexandra Silva. Algebra-coalgebra duality in brzozowski’s minimization algorithm. ACM Trans. Comput. Log., 15(1):3, 2014. Google Scholar
  4. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Coinduction up-to in a fibrational setting. In CSL-LICS, pages 20:1-20:9. ACM, 2014. Google Scholar
  5. Tomasz Brengos. On coalgebras with internal moves. In Marcello M. Bonsangue, editor, Proc. CMCS, Lecture Notes in Computer Science, pages 75-97. Springer, 2014. Google Scholar
  6. Tomasz Brengos. Lax functors and coalgebraic weak bisimulation. CoRR, abs/1404.5267, 2015. Google Scholar
  7. Tomasz Brengos. Weak bisimulation for coalgebras over order enriched monads. Logical Methods in Computer Science, 11(2:14):1-44, 2015. Google Scholar
  8. Tomasz Brengos, Marino Miculan, and Marco Peressotti. Behavioural equivalences for coalgebras with unobservable moves. Journal of Logical and Algebraic Methods in Programming, 84(6):826-852, 2015. Google Scholar
  9. Taolue Chen, Tingting Han, and Joost-Pieter Katoen. Time-abstracting bisimulation for probabilistic timed automata. In TASE, pages 177-184. IEEE Computer Society, 2008. Google Scholar
  10. Natalya Gribovskaya and Irina Virbitskaite. A categorical view of timed weak bisimulation. In TAMC, volume 6108 of Lecture Notes in Computer Science, pages 443-454. Springer, 2010. Google Scholar
  11. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic forward and backward simulations. In Proc. JSSST Annual Meeting, 2006. Google Scholar
  12. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3(4), 2007. Google Scholar
  13. Bart Jacobs. Coalgebraic trace semantics for combined possibilistic and probabilistic systems. In Proc. CMCS, Electronic Notes in Theoretical Computer Science, pages 131-152, 2008. Google Scholar
  14. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In Dirk Pattinson and Lutz Schröder, editors, Proc. CMCS, volume 7399 of Lecture Notes in Computer Science, pages 109-129. Springer, 2012. Google Scholar
  15. Marco Kick. A Mathematical Model of Timed Processes. Ph.D. dissertation, University of Edinburgh, 2003. Google Scholar
  16. Anders Kock. Strong functors and monoidal monads. Arc. Math., 23(1):113-120, 1972. Google Scholar
  17. Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 282(1):101-150, 2002. Google Scholar
  18. Stephen Lack. A 2-categories companion. Springer, 2010. Google Scholar
  19. Kim G. Larsen and Yi Wang. Time-abstracted bisimulation: Implicit specifications and decidability. Information and Computation, 134(2):75 - 101, 1997. Google Scholar
  20. Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971. Google Scholar
  21. Marino Miculan and Marco Peressotti. Structural operational semantics for non-deterministic processes with quantitative aspects. Theoretical Computer Science, 2016. Google Scholar
  22. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3-80, 2000. Google Scholar
  23. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science, 9(1), 2013. Google Scholar
  24. Alexandra Silva and Bram Westerbaan. A coalgebraic view of ε-transitions. In Reiko Heckel and Stefan Milius, editors, Proc. CALCO, volume 8089 of Lecture Notes in Computer Science, pages 267-281. Springer, 2013. Google Scholar
  25. Paweł Sobociński. Relational presheaves, change of base and weak simulation. Journal of Computer and System Sciences, 81(5):901-910, 2015. Google Scholar
  26. Sam Staton. Relating coalgebraic notions of bisimulation. Logical Methods in Computer Science, 7(1), 2011. Google Scholar
  27. Daniele Turi and Gordon Plotkin. Towards a mathematical operational semantics. In Proc. LICS, pages 280-291. IEEE Computer Society Press, 1997. Google Scholar
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