Model checking of systems with many identical timed processes

DOI10.1016/S0304-3975(01)00330-9zbMath1018.68046OpenAlexW2021255060MaRDI QIDQ1853589

Bengt Jonsson, Parosh Aziz Abdulla

Publication date: 21 January 2003

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

Full work available at URL: https://doi.org/10.1016/s0304-3975(01)00330-9

zbMATH Keywords

automatic verification of infinite state systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (13)

Liveness of Parameterized Timed Networks ⋮ On the Verification of Timed Ad Hoc Networks ⋮ Nested Timed Automata with Frozen Clocks ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ Parameterized verification of time-sensitive models of ad hoc network protocols ⋮ Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms ⋮ Monotonic Abstraction for Programs with Dynamic Memory Heaps ⋮ Parameterized model checking of weighted networks ⋮ Timed Basic Parallel Processes ⋮ Parameterized model checking of networks of timed automata with Boolean guards ⋮ Well (and Better) Quasi-Ordered Transition Systems ⋮ Unnamed Item ⋮ Network invariants for real-time systems

Uses Software

• CESAR

Cites Work

• Undecidable verification problems for programs with unreliable channels
• Decidability of a temporal logic problem for Petri nets
• Reduction and covering of infinite reachability trees
• Deciding bisimulation equivalences for a class of non-finite-state programs
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Algorithmic analysis of programs with well quasi-ordered domains.
• A structural induction theorem for processes
• Verifying programs with unreliable channels
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Recoverability of Communication Protocols--Implications of a Theoretical Study
• A really temporal logic
• Reasoning about systems with many processes
• Deciding properties of integral relational automata
• Hybrid automata with finite bisimulations
• Petri nets, commutative context-free grammars, and basic parallel processes
• Ordering by Divisibility in Abstract Algebras
• Decidability of bisimulation equivalence for normed pushdown processes
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model checking of systems with many identical timed processes