TY - GEN
T1 - DisTL
T2 - 24th Italian Conference on Theoretical Computer Science, ICTCS 2023
AU - Castiglioni, Valentina
AU - Loreti, Michele
AU - Tini, Simone
PY - 2023
Y1 - 2023
N2 - The behaviour of systems characterised by a closed interaction of software components with the environment is inevitably subject to uncertainties. We propose a general framework for the specification and verification of requirements on the behaviour of these systems. We introduce the Distribution Temporal Logic (DisTL), a novel temporal logic allowing us to specify properties on the expected behaviour of systems, and to include the presence of uncertainties in the specification. We equip DisTL with a robustness semantics and we prove it sound and complete w.r.t. the semantics induced by the evolution metric, i.e., a hemimetric expressing how well a system is fulfilling its tasks with respect to another one. Finally, we give a statistical model checking algorithm for DisTL specifications, and we apply our framework to a simple unmanned ground vehicle scenario.
AB - The behaviour of systems characterised by a closed interaction of software components with the environment is inevitably subject to uncertainties. We propose a general framework for the specification and verification of requirements on the behaviour of these systems. We introduce the Distribution Temporal Logic (DisTL), a novel temporal logic allowing us to specify properties on the expected behaviour of systems, and to include the presence of uncertainties in the specification. We equip DisTL with a robustness semantics and we prove it sound and complete w.r.t. the semantics induced by the evolution metric, i.e., a hemimetric expressing how well a system is fulfilling its tasks with respect to another one. Finally, we give a statistical model checking algorithm for DisTL specifications, and we apply our framework to a simple unmanned ground vehicle scenario.
KW - Cyber-physical systems
KW - Evolution sequence
KW - Statistical model checking
KW - Temporal logic
KW - Uncertainty
UR - http://www.scopus.com/inward/record.url?scp=85181067118&partnerID=8YFLogxK
M3 - Conference contribution
T3 - CEUR Workshop Proceedings
SP - 15
EP - 30
BT - ICTCS 2023 : Italian Conference on Theoretical Computer Science 2023
A2 - Castiglione, Giuseppa
A2 - Sciortino, Marinella
PB - CEUR-WS.org
Y2 - 13 September 2023 through 15 September 2023
ER -