Liveness of parameterized timed networks

DOI10.1007/978-3-662-47666-6_30MaRDI QIDQ3449490zbMATHOpenAlexFDO

Authors Benjamin Aminof, Sasha Rubin, Florian Zuleger, Francesco Spegni

Publication date 4 November 2015

Published in Automata, Languages, and Programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We consider the model checking problem of infinite state systems given in the form of parameterized discrete timed networks with multiple clocks. We show that this problem is decidable with respect to specifications given by B- or S-automata. Such specifications are very expressive (they strictly subsume omega-regular specifications), and easily express complex liveness and safety properties. Our results are obtained by modeling the passage of time using symmetric broadcast, and by solving the model checking problem of parameterized systems of un-timed processes communicating using k-wise rendezvous and symmetric broadcast. Our decidability proof makes use of automata theory, rational linear programming, and geometric reasoning for solving certain reachability questions in vector addition systems; we believe these proof techniques will be useful in solving related problems.

Recommendations

• Parameterized model checking of networks of timed automata with Boolean guards
• Model checking of systems with many identical timed processes
• Closed, open, and robust timed networks
• Parameterized model checking of weighted networks
• scientific article; zbMATH DE number 1701759

Cites work

• scientific article; zbMATH DE number 559221 (Why is no real title available?)
• scientific article; zbMATH DE number 2102690 (Why is no real title available?)
• Beyond $\omega$-Regular Languages
• Model checking of systems with many identical timed processes
• Parameterised verification for multi-agent systems
• Parameterized Model Checking of Token-Passing Systems
• Parameterized model checking of rendezvous systems
• Parameterized verification of ad hoc networks
• Proving properties of a ring of finite-state machines
• Reasoning about systems with many processes
• Timed verification of the generic architecture of a memory circuit using parametric timed automata

Cited in

(20)

• Parameterized model checking of rendezvous systems
• Parameterized verification of many identical probabilistic timed processes
• Verification of agent navigation in partially-known environments
• Why liveness for timed automata is hard, and what we can do about it
• Deciding fast termination for probabilistic VASS with nondeterminism
• Closed, open, and robust timed networks
• Universal safety for timed Petri nets is PSPACE-complete
• Liveness in broadcast networks
• Why liveness for timed automata is hard, and what we can do about it
• Parameterized model checking of weighted networks
• The polynomial complexity of vector addition systems with states
• Timing conditions for linearizability in uniform counting networks
• Parameterized model checking of networks of timed automata with Boolean guards
• Model checking parameterised multi-token systems via the composition method
• Model checking of systems with many identical timed processes
• scientific article; zbMATH DE number 1689043 (Why is no real title available?)
• scientific article; zbMATH DE number 1538037 (Why is no real title available?)
• Accuracy of message counting abstraction in fault-tolerant distributed algorithms
• Parametric timed broadcast protocols
• Polynomial-time optimal liveness enforcement for guidepath-based transport systems

This page was built for publication: Liveness of parameterized timed networks

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