Parameterized model checking of networks of timed automata with Boolean guards

DOI10.1016/J.TCS.2019.12.026MaRDI QIDQ1989334zbMATH OpenOpenAlexFDO

Authors Luca Spalazzi, Francesco Spegni

Publication date 21 April 2020

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2019.12.026

zbMATH Keywords

cutoff theoremsparameterized model checkingparameterized systemstimed automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Parameterized model checking of rendezvous systems
• Parameterized model checking of rendezvous systems
• Parameterized verification of systems with global synchronization and guards
• Liveness of parameterized timed networks
• Parameterized compositional model checking

Cites work

• A theory of timed automata
• Accuracy of message counting abstraction in fault-tolerant distributed algorithms
• Analyzing guarded protocols: better cutoffs, more systems, more expressivity
• Complexity of some problems in Petri nets
• CONCUR 2004 - Concurrency Theory
• Decidability of parameterized verification
• Exact and efficient verification of parameterized cache coherence protocols
• scientific article; zbMATH DE number 1614699 (Why is no real title available?)
• scientific article; zbMATH DE number 1755138 (Why is no real title available?)
• Liveness of parameterized timed networks
• Model checking and abstraction to the aid of parameterized systems (a survey)
• Model checking of systems with many identical timed processes
• Model Checking Real-Time Systems
• On Reasoning About Rings
• Parameterised model checking for alternating-time temporal logic
• Parameterised verification for multi-agent systems
• Parameterized model checking of rendezvous systems
• Parameterized model checking of synchronous distributed algorithms by abstraction
• Parameterized Model Checking of Token-Passing Systems
• Probabilistic clock synchronization
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Reasoning about systems with many processes
• The benefits of relaxing punctuality
• Verification of parametric concurrent systems with prioritised FIFO resource management

Cited in

(12)

• Parameterized model checking of rendezvous systems
• A counter abstraction technique for verifying properties of probabilistic swarm systems
• Parameterized verification of systems with global synchronization and guards
• Tight cutoffs for guarded protocols with fairness
• Incremental Language Inclusion Checking for Networks of Timed Automata
• Parameterized verification of many identical probabilistic timed processes
• Statistical Model Checking for Networks of Priced Timed Automata
• Parameterized model checking of rendezvous systems
• Analyzing guarded protocols: better cutoffs, more systems, more expressivity
• An abstraction technique for parameterized model checking of leader election protocols: application to FTSP
• Liveness of parameterized timed networks
• Parameterized model-checking of discrete-timed networks and symmetric-broadcast systems

This page was built for publication: Parameterized model checking of networks of timed automata with Boolean guards

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