Propositional Dynamic Logic for Message-Passing Systems

DOI10.1007/978-3-540-77050-3_25MaRDI QIDQ5458843zbMATH OpenOpenAlexFDO

Authors Benedikt Bollig, Ingmar Meinecke, Dietrich Kuske

Publication date 24 April 2008

Published in FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.4764

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We examine a bidirectional propositional dynamic logic (PDL) for finite and infinite message sequence charts (MSCs) extending LTL and TLC-. By this kind of multi-modal logic we can express properties both in the entire future and in the past of an event. Path expressions strengthen the classical until operator of temporal logic. For every formula defining an MSC language, we construct a communicating finite-state machine (CFM) accepting the same language. The CFM obtained has size exponential in the size of the formula. This synthesis problem is solved in full generality, i.e., also for MSCs with unbounded channels. The model checking problem for CFMs and HMSCs turns out to be in PSPACE for existentially bounded MSCs. Finally, we show that, for PDL with intersection, the semantics of a formula cannot be captured by a CFM anymore.

Recommendations

• Propositional dynamic logic for message-passing systems
• Propositional dynamic logic with converse and repeat for message-passing systems
• Propositional dynamic logic with converse and repeat for message-passing systems
• Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic
• scientific article; zbMATH DE number 1954389

Cites work

• A Kleene theorem and model checking algorithms for existentially bounded communicating automata
• A product version of dynamic linear time temporal logic
• Dynamic linear time temporal logic
• scientific article; zbMATH DE number 1670846 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 2081110 (Why is no real title available?)
• scientific article; zbMATH DE number 1479635 (Why is no real title available?)
• scientific article; zbMATH DE number 2086660 (Why is no real title available?)
• Message-passing automata are expressively equivalent to EMSO logic
• Muller message-passing automata and logics
• On Communicating Finite-State Machines
• Propositional Dynamic Logic for Message-Passing Systems
• Propositional dynamic logic of regular programs
• Reasoning about layered message passing systems
• Satisfiability and model checking for MSO-definable temporal logics are in PSPACE.

Cited in

(11)

• A message-passing interpretation of adjoint logic
• Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic
• A logic framework for reasoning with movement based on fuzzy qualitative representation
• Propositional dynamic logic for message-passing systems
• A Complete Quantified Epistemic Logic for Reasoning about Message Passing Systems
• A parametrized propositional dynamic logic with application to service synthesis
• It is easy to be wise after the event: communicating finite-state machines capture first-order logic with ``happened before
• CONCUR 2004 - Concurrency Theory
• Propositional Dynamic Logic for Message-Passing Systems
• Propositional dynamic logic with converse and repeat for message-passing systems
• Propositional dynamic logic with converse and repeat for message-passing systems

This page was built for publication: Propositional Dynamic Logic for Message-Passing Systems

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