Deductive verification of alternating systems
From MaRDI portal
Publication:939163
DOI10.1007/s00165-008-0075-6zbMath1152.68032OpenAlexW2150498345MaRDI QIDQ939163
Zohar Manna, Henny B. Sipma, Matteo Slanina
Publication date: 21 August 2008
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-008-0075-6
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Uses Software
Cites Work
- Secure protocol composition
- The strict determinateness of certain infinite games
- The temporal logic of branching time
- Results on the propositional \(\mu\)-calculus
- Compositional analysis of contract-signing protocols
- Formal analysis of multiparty contract signing
- Deductive verification of alternating systems
- Using branching time temporal logic to synthesize synchronization skeletons
- The \(\mu\)-calculus as an assertion-language for fairness arguments
- Borel determinacy
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Infinite games played on finite graphs
- Automatic generation of invariants and intermediate assertions
- A compositional approach to CTL\(^*\) verification
- Verification of concurrent programs: The automata-theoretic framework
- Complete axiomatization and decidability of alternating-time temporal logic
- An axiomatization of full Computation Tree Logic
- Generalized temporal verification diagrams
- Alternating-time temporal logic
- Proving ATL* Properties of Infinite-State Systems
- Temporal Verification of Reactive Systems: Response
- “Sometimes” and “not never” revisited
- Alternation
- Soundness and Completeness of an Axiom System for Program Verification
- Optimistic fair exchange of digital signatures
- On the synthesis of strategies in infinite games
- On the error term of an asymptotic formula of Ramanujan
- Verification of temporal properties
- An axiomatic basis for computer programming
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
