Maximality-based Labeled Stochastic Transition Systems
(MLSTS) was presented [6, 11] as a new semantic model for characterizing the functional and performance properties of concurrent systems, under the assumption of arbitrarily distributed (i.e. non-Markovian) durations of actions. The MLSTS models can be automatically generated from S-LOTOS specifications according to the (true concurrency) maximality semantics . The main advantage is to pruning the state graph without loss of information w.r.t. ST-semantic models . As a first work on MLSTS, we focus in this paper on in the verification of functional properties of systems, using a variant of model-checking technique.