Reasoning about networks with many identical finite state processes
From MaRDI portal
Publication:921983
DOI10.1016/0890-5401(89)90026-6zbMATH Open0709.68610OpenAlexW1982900911MaRDI QIDQ921983FDOQ921983
M. C. Browne, Orna Grumberg, Edmund 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
Cites Work
- Characterizing finite Kripke structures in propositional temporal logic
- The complexity of propositional linear temporal logics
- Title not available (Why is that?)
- A calculus of communicating systems
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- “Sometimes” and “not never” revisited
- Title not available (Why is that?)
- A multiprocess network logic with temporal and spatial modalities
- Title not available (Why is that?)
- Automatic Verification of Sequential Circuits Using Temporal Logic
- Title not available (Why is that?)
- Invariance and non-determinacy
- Title not available (Why is that?)
Cited In (29)
- Parameterised verification for multi-agent systems
- Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
- Efficient SAT-based bounded model checking for software verification
- The Birth of Model Checking
- Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
- Checking deadlock-freedom of parametric component-based systems
- Parameterized model checking of rendezvous systems
- Networks of Processes with Parameterized State Space
- Computing parameterized invariants of parameterized Petri nets
- Symbolic model checking with rich assertional languages
- Parameterized model checking on the TSO weak memory model
- Checking extended CTL properties using guarded quotient structures
- Verification of component-based systems with recursive architectures
- Model Checking Parameterised Multi-token Systems via the Composition Method
- On temporal logics with data variable quantifications: decidability and complexity
- Automatic verification of a class of systolic circuits
- Synthesis of large dynamic concurrent programs from dynamic specifications
- On Reasoning About Rings
- Structural Invariants for the Verification of Systems with Parameterized Architectures
- An automatic abstraction technique for verifying featured, parameterised systems
- Parametrized invariance for infinite state processes
- Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
- Deadlock analysis in networks of communicating processes
- Model checking transactional memories
- Automatic verification for a class of distributed systems
- Computing Parameterized Invariants of Parameterized Petri Nets
- Model Checking Parameterized Systems
- Deciding bisimulation and trace equivalences for systems with many identical processes
- Priority systems with many identical processes
Uses Software
This page was built for publication: Reasoning about networks with many identical finite state processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q921983)