Comparative Branching-Time Semantics

d Abstract) Christel Baier1 , Holger Hermanns2,3 , Joost-Pieter Katoen2 , and Verena Wolf1 1 Institut f¨ur Informatik I, University of Bonn R¨omerstraße 164, D-53117 Bonn, Germany 2 Department of Computer Science, University of Twente P.O. Box 217, 7500 AE Enschede, The Netherlands 3 Department of Computer Science Saarland University, D-66123 Saarbr¨ucken, Germany This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterised in terms of the temporal logics PCTL and CSL. Apart from presenting various existing branching-time relations in a uniform manner, our contributions are: (i) weak simulation for DTMCs is defined, (ii) weak bisimulation equivalence is shown to coincide with weak simulation equivalence, (iii) logical characterisation of weak (bi)simulations are provided, and (iv) a classificat...

• Type: Conference
• Year: 2003
• Where: CONCUR
• Authors: Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Verena Wolf
• Keywords: Branching-time Relations, CONCUR 2003, Weak Bisimulation Equivalence, Weak Simulation