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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Akshay, S., Bollig, B., & Gastin, P. (2007). Automata and logics for timed message sequence charts. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4855 LNCS, pp. 290–302). Springer Verlag. https://doi.org/10.1007/978-3-540-77050-3_24
Mendeley helps you to discover research relevant for your work.