A Faster-Than Relation for Semi-Markov Decision Processes

Mathias Ruggaard Pedersen
(Aalborg University)
Giorgio Bacci
(Aalborg University)
Kim Guldstrand Larsen
(Aalborg University)

When modeling concurrent or cyber-physical systems, non-functional requirements such as time are important to consider. In order to improve the timing aspects of a model, it is necessary to have some notion of what it means for a process to be faster than another, which can guide the stepwise refinement of the model. To this end we study a faster-than relation for semi-Markov decision processes and compare it to standard notions for relating systems. We consider the compositional aspects of this relation, and show that the faster-than relation is not a precongruence with respect to parallel composition, hence giving rise to so-called parallel timing anomalies. We take the first steps toward understanding this problem by identifying decidable conditions sufficient to avoid parallel timing anomalies in the absence of non-determinism.

In Alessandro Aldini and Herbert Wiklicky: Proceedings 16th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2019), Prague, Czech Republic, 7th April 2019, Electronic Proceedings in Theoretical Computer Science 312, pp. 29–42.
Published: 20th January 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.312.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org