Michael Huth, Imperial College, London (United Kingdom)

 

p-Automata: New Foundations for Discrete-Time Probabilistic Verification

 

Michael Huth, Imperial College, London (United Kingdom)

 

Abstract:

In the automata-based approach to verification, an automaton accepts
as its language a set of models. This approach comes with a host of
important techniques that make it widely used: specifications and
models alike have meaning-preserving representations as automata,
model checking reduces to acceptance of input for an automaton,
satisfiability and validity checking reduce to emptiness and
universality checks of automata (respectively), automata are closed
under Boolean operations,
model refinement reduces to language containment, and simulations
efficiently under-approximate language containment.

We develop such an automata-based approach to probabilistic
verification that supports all techniques aforementioned, where models
are countable, discrete-time, labeled Markov chains and probabilistic
specifications subsume all formulas written in probabilistic
computation tree logic.

 

(This is joint work with Nir Piterman and Daniel Wagner).