Parameterized model checking of networks of timed automata with Boolean guards

DOI10.1016/j.tcs.2019.12.026zbMath1433.68219OpenAlexW2997159042MaRDI QIDQ1989334

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

timed automataparameterized systemsparameterized model checkingcutoff theorems

Mathematics Subject Classification ID

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

Related Items (2)

A counter abstraction technique for verifying properties of probabilistic swarm systems ⋮ Parameterized model checking of rendezvous systems

Cites Work

• Unnamed Item
• Unnamed Item
• Parameterised verification for multi-agent systems
• Probabilistic clock synchronization
• Complexity of some problems in Petri nets
• A theory of timed automata
• Parameterized model checking of rendezvous systems
• Model checking of systems with many identical timed processes
• Model checking and abstraction to the aid of parameterized systems (a survey)
• Verification of parametric concurrent systems with prioritised FIFO resource management
• Parameterized Model Checking of Token-Passing Systems
• Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
• Model Checking Real-Time Systems
• Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
• Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity
• Liveness of Parameterized Timed Networks
• Reasoning about systems with many processes
• The benefits of relaxing punctuality
• Decidability of Parameterized Verification
• Parameterised Model Checking for Alternating-Time Temporal Logic.
• CONCUR 2004 - Concurrency Theory
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• On Reasoning About Rings
• Correct Hardware Design and Verification Methods

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