Automata and Logics for Timed Message Sequence Charts

DOI10.1007/978-3-540-77050-3_24MaRDI QIDQ5458842zbMATH OpenOpenAlexFDO

Authors S. Akshay, Benedikt Bollig, Paul Gastin

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://doi.org/10.1007/978-3-540-77050-3_24

Mathematics Subject Classification ID

Logic in computer science (03B70) Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Timed semantics of message sequence charts based on timed automata
• Model checking time-constrained scenario-based specifications
• Event clock message passing automata: a logical characterization and an emptiness checking algorithm
• scientific article; zbMATH DE number 1760052
• Checking Coverage for Infinite Collections of Timed Scenarios

Cites work

• A Kleene theorem and model checking algorithms for existentially bounded communicating automata
• A Logical Characterisation of Event Clock Automata
• A theory of regular MSC languages
• A theory of timed automata
• Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
• Event-clock automata: a determinizable class of timed automata
• scientific article; zbMATH DE number 1500642 (Why is no real title available?)
• Matching Scenarios with Timing Constraints
• Message-passing automata are expressively equivalent to EMSO logic
• On Communicating Finite-State Machines
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(7)

• Event clock message passing automata: a logical characterization and an emptiness checking algorithm
• Checking conformance for time-constrained scenario-based specifications
• SMT-based scenario verification for hybrid systems
• Timed semantics of message sequence charts based on timed automata
• Checking Coverage for Infinite Collections of Timed Scenarios
• A concurrency-preserving translation from time Petri nets to networks of timed automata
• Proving sequential function chart programs using timed automata

This page was built for publication: Automata and Logics for Timed Message Sequence Charts

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