Reasoning about networks with many identical finite state processes

DOI10.1016/0890-5401(89)90026-6zbMath0709.68610OpenAlexW1982900911MaRDI QIDQ921983

M. C. Browne, Orna Grumberg, Edmund M. Clarke

Publication date: 1989

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(89)90026-6

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items

Structural Invariants for the Verification of Systems with Parameterized Architectures ⋮ Computing Parameterized Invariants of Parameterized Petri Nets ⋮ Parameterized model checking of rendezvous systems ⋮ Model checking transactional memories ⋮ Model Checking Parameterized Systems ⋮ Deadlock analysis in networks of communicating processes ⋮ On temporal logics with data variable quantifications: decidability and complexity ⋮ Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ The Birth of Model Checking ⋮ Parameterized model checking on the TSO weak memory model ⋮ Verification of component-based systems with recursive architectures ⋮ Automatic verification for a class of distributed systems ⋮ On Reasoning About Rings ⋮ Checking extended CTL properties using guarded quotient structures ⋮ Parametrized invariance for infinite state processes ⋮ Deciding bisimulation and trace equivalences for systems with many identical processes ⋮ Automatic verification of a class of systolic circuits ⋮ An automatic abstraction technique for verifying featured, parameterised systems ⋮ Efficient SAT-based bounded model checking for software verification ⋮ Checking deadlock-freedom of parametric component-based systems ⋮ Networks of Processes with Parameterized State Space ⋮ Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Symbolic model checking with rich assertional languages ⋮ Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems ⋮ Model Checking Parameterised Multi-token Systems via the Composition Method ⋮ Priority systems with many identical processes ⋮ Parameterised verification for multi-agent systems ⋮ Computing parameterized invariants of parameterized Petri nets

Uses Software

• CESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A multiprocess network logic with temporal and spatial modalities
• Characterizing finite Kripke structures in propositional temporal logic
• A calculus of communicating systems
• Invariance and non-determinacy
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Automatic Verification of Sequential Circuits Using Temporal Logic
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics