Abstract

Maximality-based Labeled Stochastic Transition Systems (MLSTS)
was presented 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.

Information

Item Type:	Journal
Divisions:
ePrint ID:	165
Date Deposited:	2014-12-08
Further Information:	Google Scholar
URI:	https://www.univ-soukahras.dz/en/publication/article/165

BibTex