On Reasoning About Rings

DOI10.1142/S0129054103001881zbMath1101.68371MaRDI QIDQ5696925

Kedar S. Namjoshi, E. Allen Emerson

Publication date: 19 October 2005

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Distributed systems (68M14) Network protocols (68M12)

Related Items

Formal verification of mobile robot protocols ⋮ Local Symmetry and Compositional Verification ⋮ Compositional analysis for verification of parameterized systems ⋮ Parameterized Verification of Communicating Automata under Context Bounds ⋮ Parameterized model checking of rendezvous systems ⋮ Verification of agent navigation in partially-known environments ⋮ On notions of regularity for data languages ⋮ Compositional verification of smart contracts through communication abstraction ⋮ Feature interaction detection by pairwise analysis of LTL properties -- A case study ⋮ On temporal logics with data variable quantifications: decidability and complexity ⋮ An invariant-based approach to the verification of asynchronous parameterized networks ⋮ Model and program repair via group actions ⋮ Parameterized verification of time-sensitive models of ad hoc network protocols ⋮ \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms ⋮ An automata-theoretic approach to the verification of distributed algorithms ⋮ Learning Meets Verification ⋮ On pebble automata for data languages with decidable emptiness problem ⋮ Parametrized invariance for infinite state processes ⋮ Multi-parameterised compositional verification of safety properties ⋮ Parameterized model checking of networks of timed automata with Boolean guards ⋮ Regular Model Checking using Widening Techniques ⋮ Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Symbolic model checking with rich assertional languages ⋮ Automatic verification of parameterized networks of processes ⋮ An approach to the verification of symmetric parameterized distributed systems ⋮ View abstraction for systems with component identities ⋮ Liveness by Invisible Invariants ⋮ On Verifying Fault Tolerance of Distributed Protocols ⋮ Verification of Parameterized Communicating Automata via Split-Width ⋮ Parameterized synthesis of self-stabilizing protocols in symmetric networks ⋮ Model Checking Parameterised Multi-token Systems via the Composition Method ⋮ Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings

Cites Work

• Unnamed Item
• Unnamed Item
• Reasoning about networks with many identical finite state processes
• Characterizing finite Kripke structures in propositional temporal logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited

This page was built for publication: On Reasoning About Rings