Reachability of communicating timed processes

DOI10.1007/978-3-642-37075-5_6MaRDI QIDQ4910413zbMATH OpenOpenAlexFDO

Authors Lorenzo Clemente, Frédéric Herbreteau, Amélie Stainer, Grégoire Sutre

Publication date 18 March 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1209.0571

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We study the reachability problem for communicating timed processes, both in discrete and dense time. Our model comprises automata with local timing constraints communicating over unbounded FIFO channels. Each automaton can only access its set of local clocks; all clocks evolve at the same rate. Our main contribution is a complete characterization of decidable and undecidable communication topologies, for both discrete and dense time. We also obtain complexity results, by showing that communicating timed processes are at least as hard as Petri nets; in the discrete time, we also show equivalence with Petri nets. Our results follow from mutual topology-preserving reductions between timed automata and (untimed) counter automata.

Recommendations

• Perfect timed communication is hard
• Decidable topologies for communicating automata with FIFO and bag channels
• Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
• Model checking of systems with many identical timed processes
• Reachability in timed counter systems

Cited in

(10)

• Perfect timed communication is hard
• Combining free choice and time in Petri nets
• Decidable classes of unbounded Petri nets with time and urgency
• Safety verification of communicating one-counter machines
• Decidable topologies for communicating automata with FIFO and bag channels
• scientific article; zbMATH DE number 4011913 (Why is no real title available?)
• scientific article; zbMATH DE number 1759782 (Why is no real title available?)
• Progress-preserving refinements of CTA
• Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
• Timed Basic Parallel Processes

This page was built for publication: Reachability of communicating timed processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4910413)