Event clock message passing automata: a logical characterization and an emptiness checking algorithm

DOI10.1007/s10703-012-0179-8zbMath1291.68239OpenAlexW2045909926MaRDI QIDQ2248059

S. Akshay, Paul Gastin, Benedikt Bollig

Publication date: 30 June 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-012-0179-8

zbMATH Keywords

timed automataMSO logicmessage sequence chartsmessage passing automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Unnamed Item
• Event-clock automata: a determinizable class of timed automata
• A theory of timed automata
• Bounded MSC communication
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• A Kleene theorem and model checking algorithms for existentially bounded communicating automata
• Message-passing automata are expressively equivalent to EMSO logic
• A theory of regular MSC languages
• Weak Second‐Order Arithmetic and Finite Automata
• Matching Scenarios with Timing Constraints
• Timed Unfoldings for Networks of Timed Automata
• On Communicating Finite-State Machines
• Decision Problems of Finite Automata Design and Related Arithmetics
• The Theory of Message Sequence Charts
• Automata and Logics for Timed Message Sequence Charts
• A Logical Characterisation of Event Clock Automata
• Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
• Formal Modeling and Analysis of Timed Systems