Congruences and bisimulations for continuous-time stochastic logic
Continuous stochastic logic (CSL) deals with the verification of systems operating in continuous time, it may be traced to the well known tree logic CTL. We propose a probabilistic interpretation of this logic that is based on stochastic relations without making specific assumptions on the underlying distribution, and study the problem of bisimulations in a fairly general context from the viewpoint of congruences for stochastic relations. The goal is finding minimal sets of formulas that permit efficient checking of models. © Springer-Verlag Berlin Heidelberg 2005.