Computer Aided Verification

DOI10.1007/b98490zbMath1103.68614OpenAlexW4298302743MaRDI QIDQ5312933

Peter Gammie, Ron van der Meyden

Publication date: 25 August 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b98490

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (33)

Formalising privacy policies in social networks ⋮ Quantified epistemic logics for reasoning about knowledge in multi-agent systems ⋮ Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams ⋮ Checking EMTLK properties of timed interpreted systems via bounded model checking ⋮ A computationally grounded, weighted doxastic logic ⋮ Practical verification of multi-agent systems against \textsc{Slk} specifications ⋮ Verifying Real-Time Properties of Multi-agent Systems via SMT-Based Bounded Model Checking ⋮ Combined model checking for temporal, probabilistic, and real-time logics ⋮ To know or not to know: Epistemic approaches to security protocol verification ⋮ Program semantics and verification technique for AI-centred programs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A first-order coalition logic for BDI-agents ⋮ Populational announcement logic (PPAL) ⋮ Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types ⋮ Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol ⋮ Automatic Data-Abstraction in Model Checking Multi-Agent Systems ⋮ Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic ⋮ Symbolic Model Checking the Knowledge in Herbivore Protocol ⋮ Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems ⋮ Producing explanations for rich logics ⋮ Model-based safety assessment of a triple modular generator with xSAP ⋮ A Complete Quantified Epistemic Logic for Reasoning about Message Passing Systems ⋮ Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic ⋮ Approximate verification of strategic abilities under imperfect information ⋮ Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments ⋮ First-Order Linear-Time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment ⋮ An Epistemic Predicate CTL* for Finite Control π-Processes ⋮ Bounded model checking for knowledge and real time ⋮ Verification and strategy synthesis for coalition announcement logic ⋮ A Three-Value Abstraction Technique for the Verification of Epistemic Properties in Multi-agent Systems ⋮ Terminal satisfiability in GSTE

Uses Software

• MCK

This page was built for publication: Computer Aided Verification