Selected publications at LSV: 2007

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 second-order 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.

@inproceedings{ABG-fsttcs07,
   address = {New~Delhi, India},
   author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul},
   booktitle = {{P}roceedings of the 27th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'07)},
   DOI = {10.1007/978-3-540-77050-3_24},
   editor = {Arvind, V. and Prasad, Sanjiva},
   month = dec,
   pages = {290-302},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Automata and Logics for Timed Message Sequence Charts},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
   volume = {4855},
   year = {2007},
}

About LSV