Symbolic model checking of public announcement protocols

DOI10.1093/LOGCOM/EXZ023MaRDI QIDQ5216337zbMATH OpenOpenAlexWikidataFDO

Authors Tristan Charrier, Sophie Pinchinat, François Schwarzentruber

Publication date 17 February 2020

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/exz023

zbMATH Keywords

arbitrary public announcementsepistemic logicmodel checkingsymbolic models

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Symbolic Model Checking Commitment Protocols Using Reduction
• scientific article; zbMATH DE number 1507203
• scientific article; zbMATH DE number 1222405
• A symbolic semantics for abstract model checking
• Parameterized verification and model checking for distributed broadcast protocols
• Symbolic model checking the knowledge in Herbivore protocol
• Symbolic model checking in non-Boolean domains

Cited in

(6)

• Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment
• A computationally grounded logic of graded belief
• Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness
• AI 2005: Advances in Artificial Intelligence
• Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic
• Model Checking for Coalition Announcement Logic

This page was built for publication: Symbolic model checking of public announcement protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5216337)