Home
Scholarly Works
A dynamic temporal logic for quality of service in...
Journal article

A dynamic temporal logic for quality of service in choreographic models

Abstract

We propose a framework for expressing and analysing the Quality of Service (QoS) of message-passing systems using a choreographic model that consists of g-choreographies and Communicating Finite State machines (CFSMs). Our main contributions are: (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) a bounded model-checking algorithm to verify QoS property of communicating systems.

Authors

Pombo CGL; Martinez-Suñé AE; Tuosto E

Journal

Theoretical Computer Science, Vol. 1043, ,

Publisher

Elsevier

Publication Date

July 30, 2025

DOI

10.1016/j.tcs.2025.115247

ISSN

0304-3975

Contact the Experts team