2018/10/31 by Mathias Ruggaard Pedersen, Giorgio Bacci, Kim Guldstrand Larsen
Computer Science · #cs.FL
paper · pdf · doi:10.4204/eptcs.312.3
published as EPTCS 312, 2020, pp. 29-42 · In Proceedings QAPL 2019, arXiv:2001.06163
arxiv created 2020/01/20 · arxiv updated 2020/01/22
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.