A Dynamic Temporal Logic for Quality of Service in Choreographic Models
Abstract
We propose a framework for expressing and analyzing the Quality of Service (QoS) of message-passing systems using a choreographic model that consists of g-choreographies and Communicating Finite State machines (CFSMs). The following are our three main contributions: (I) an extension of CFSMs with non-functional contracts to specify quantitative constraints of local computations, (II) a dynamic temporal logic capable of expressing QoS, properties of systems relative to the g-choreography that specifies the communication protocol, (III) the semi-decidability of our logic which enables a bounded model-checking approach to verify QoS property of communicating systems.
Keywords
Cite
@article{arxiv.2311.01414,
title = {A Dynamic Temporal Logic for Quality of Service in Choreographic Models},
author = {Carlos G. Lopez Pombo and Agustín E. Martinez Suñé and Emilio Tuosto},
journal= {arXiv preprint arXiv:2311.01414},
year = {2023}
}
Comments
20 pages, Accepted for publication at International Conference on Theoretical Aspects of Computing 2023