Model checking of systems with many identical timed processes

DOI10.1016/S0304-3975(01)00330-9zbMath1018.68046MaRDI 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

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

Related Items

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

Uses Software

• CESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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