Sciweavers

Share
FSTTCS
2007
Springer

Automata and Logics for Timed Message Sequence Charts

11 years 11 months ago
Automata and Logics for Timed Message Sequence Charts
Abstract. We provide a framework for distributed systems that impose timing constraints on their executions. We propose a timed model of communicating finite-state machines, which communicate by exchanging messages through channels and use event clocks to generate collections of timed message sequence charts (T-MSCs). As a specification language, we propose a monadic secondorder logic equipped with timing predicates and interpreted over T-MSCs. We establish expressive equivalence of our automata and logic. Moreover, we prove that, for (existentially) bounded channels, emptiness and satisfiability are decidable for our automata and logic.
S. Akshay, Benedikt Bollig, Paul Gastin
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FSTTCS
Authors S. Akshay, Benedikt Bollig, Paul Gastin
Comments (0)
books