We propose a new infinite-state model, called the Multi-queue Discrete limed Automaton MQDTA, which extends Timed Automata with queues, but only has integer-valued clocks. Due to careful restrictions on queue usage, the binary reachability (the set of all pairs of configurations (α,β) of an MQDTA such that α can reach β through zero or more transitions) is effectively semilinear. We then prove the decidability of a class of Presburger formulae defined over the binary reachability, allowing the automatic verification of many interesting properties of a MQDTA. The MQDTA model can be used to specify and verify various systems with unbounded queues, such as a real-time scheduler. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
San Pietro, P., & Dang, Z. (2003). Automatic verification of multi-queue discrete Timed Automata. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2697, 159–171. https://doi.org/10.1007/3-540-45071-8_18
Mendeley helps you to discover research relevant for your work.