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.

• Type: Conference
• Year: 2007
• Where: FSTTCS
• Authors: S. Akshay, Benedikt Bollig, Paul Gastin
• Keywords: FSTTCS 2007, Monadic Secondorder Logic, Timed Message Sequence, Timed Model