A Kleene theorem and model checking algorithms for existentially bounded communicating automata

DOI10.1016/j.ic.2006.01.005zbMath1104.68066MaRDI QIDQ2496297

Anca Muscholl, Dietrich Kuske, Blaise Genest

Publication date: 12 July 2006

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2006.01.005

zbMATH Keywords

model checking; message sequence charts; Kleene theorem; communicating finite state machines

Mathematics Subject Classification ID

68W05: Nonnumerical algorithms

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Propositional Dynamic Logic for Message-Passing Systems, Synthesis of Safe Message-Passing Systems, Automata and Logics for Timed Message Sequence Charts, Regular set of representatives for time-constrained MSC graphs, Compositional synthesis of asynchronous automata, Causal message sequence charts, Muller message-passing automata and logics, Distributed Asynchronous Automata, Realizability of Concurrent Recursive Programs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Logical definability on infinite traces
• Verifying lossy channel systems has nonprimitive recursive complexity.
• Bounded MSC communication
• Regular sets of infinite message sequence charts
• Verifying programs with unreliable channels
• Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
• A theory of regular MSC languages
• On Communicating Finite-State Machines
• Notes on finite asynchronous automata
• Tools and Algorithms for the Construction and Analysis of Systems
• CONCUR 2004 - Concurrency Theory
• Well-structured transition systems everywhere!