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

68M14: Distributed systems

68M12: Network protocols

Related Items

Regular Model Checking using Widening Techniques, Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms, On Verifying Fault Tolerance of Distributed Protocols, Symbolic model checking with rich assertional languages, Automatic verification of parameterized networks of processes, On temporal logics with data variable quantifications: decidability and complexity, Parametrized invariance for infinite state processes, Multi-parameterised compositional verification of safety properties, An invariant-based approach to the verification of asynchronous parameterized networks, On notions of regularity for data languages, Feature interaction detection by pairwise analysis of LTL properties -- A case study, Parameterized verification of time-sensitive models of ad hoc network protocols, Parameterized model checking of rendezvous systems, \(\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, On pebble automata for data languages with decidable emptiness problem, Parameterized model checking of networks of timed automata with Boolean guards, View abstraction for systems with component identities, Parameterized synthesis of self-stabilizing protocols in symmetric networks, Formal verification of mobile robot protocols, Compositional analysis for verification of parameterized systems, An approach to the verification of symmetric parameterized distributed systems, Verification of Parameterized Communicating Automata via Split-Width, Model Checking Parameterised Multi-token Systems via the Composition Method, Local Symmetry and Compositional Verification, Parameterized Verification of Communicating Automata under Context Bounds, Learning Meets Verification, Liveness by Invisible Invariants

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