Author name cluster

Thierry Massart

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

Highlights Conference 2013 Conference Abstract

Synchronization in Markov decision processes

Mahsa Shirmohammadi
Laurent Doyen
Thierry Massart

Markov Decision Processes (MDPs) are 1-1/2 player stochastic games. The player tries to maximize the probability to satisfy an objective. Traditionally, the objective of the player is expressed as a set of desired sequences of states visited during the game. Recently, MDPs are viewed as generators of probability distributions over states, and objectives are defined as sets of sequences of probability distributions. We study synchronizing objectives that require that some state tend to accumulate all the probability mass. We consider three winning modes: sure, almost-sure and limit-sure.

PDF Details

MFCS Conference 2011 Conference Paper

Infinite Synchronizing Words for Probabilistic Automata

Laurent Doyen 0001
Thierry Massart
Mahsa Shirmohammadi

Abstract Probabilistic automata are finite-state automata where the transitions are chosen according to fixed probability distributions. We consider a semantics where on an input word the automaton produces a sequence of probability distributions over states. An infinite word is accepted if the produced sequence is synchronizing, i. e. the sequence of the highest probability in the distributions tends to 1. We show that this semantics generalizes the classical notion of synchronizing words for deterministic automata. We consider the emptiness problem, which asks whether some word is accepted by a given probabilistic automaton, and the universality problem, which asks whether all words are accepted. We provide reductions to establish the PSPACE-completeness of the two problems.

Details

LOPSTR Conference 2000 Conference Paper

Infinite State Model Checking by Abstract Interpretation and Program Specialisation

Michael Leuschel
Thierry Massart

Abstract We illustrate the use of logic programming techniques for finite model checking of CTL formulae. We present a technique for infinite state model checking of safety properties based upon logic program specialisation and analysis techniques. The power of the approach is illustrated on several examples. For that, the efficient tools logen and ecce are used. We discuss how this approach has to be extended to handle more complicated infinite state systems and to handle arbitrary CTL formulae.

Details