Liveness of parameterized timed networks

DOI10.1007/978-3-662-47666-6_30zbMATH Open1440.68170arXiv1609.04176OpenAlexW2296248291MaRDI QIDQ3449490FDOQ3449490

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)

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.

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

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

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)

Cites Work

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

Cited In (20)

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

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)