On the complexity of verification of time-sensitive distributed systems

DOI10.1007/978-3-030-91631-2_14zbMATH Open1498.68161arXiv2105.03531OpenAlexW3217038706MaRDI QIDQ2154017FDOQ2154017

Authors: Tajana Ban Kirigin, Vivek Nigam, Carolyn Talcott, Max Kanovich, Andre Scedrov 

Publication date: 13 July 2022

Abstract: This paper develops a Multiset Rewriting language with explicit time for the specification and analysis of Time-Sensitive Distributed Systems (TSDS). Goals are often specified using explicit time constraints. A good trace is an infinite trace in which the goals are satisfied perpetually despite possible interference from the environment. In our previous work (FORMATS 2016), we discussed two desirable properties of TSDSes, realizability (there exists a good trace) and survivability (where, in addition, all admissible traces are good). Here we consider two additional properties, recoverability (all compliant traces do not reach points-of-no-return) and reliability (the system can always continue functioning using a good trace). Following (FORMATS 2016), we focus on a class of systems called Progressing Timed Systems (PTS), where intuitively only a finite number of actions can be carried out in a bounded time period. We prove that for this class of systems the properties of recoverability and reliability coincide and are PSPACE-complete. Moreover, if we impose a bound on time (as in bounded model-checking), we show that for PTS the reliability property is in the $P{i}_2^p$ class of the polynomial hierarchy, a subclass of PSPACE. We also show that the bounded survivability is both NP-hard and coNP-hard.

Full work available at URL: https://arxiv.org/abs/2105.03531

Recommendations

• Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
• Decidable properties for monadic abstract state machines
• Temporal logics for the specification of performance and reliability
• Model checking of systems with many identical timed processes
• Robust Model-Checking of Linear-Time Properties in Timed Automata

zbMATH Keywords

complexitymultiset rewritingtime-sensitive distributed systems

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14)

Cites Work

• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Formal Methods for the Design of Real-Time Systems
• Title not available (Why is that?)
• On the expressivity and complexity of quantitative branching-time temporal logics
• Title not available (Why is that?)
• On the security of public key protocols
• Recognizing safety and liveness
• Tools and Algorithms for the Construction and Analysis of Systems
• A rewriting framework and logic for activities subject to regulations
• Bounded memory Dolev-Yao adversaries in collaborative systems
• Collaborative planning with confidentiality
• Quantitative temporal logics over the reals: PSpace and below
• Model Checking Quantitative Linear Time Logic
• Abstraction and completeness for real-time Maude
• Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
• A rewriting framework for activities subject to regulations

Cited In (6)

• Multi-scale verification of distributed synchronisation
• On the complexity of verifying concurrent transition systems
• Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
• Title not available (Why is that?)
• A semantic model for interacting cyber-physical systems
• On the formalization and computational complexity of resilience problems for cyber-physical systems

This page was built for publication: On the complexity of verification of time-sensitive distributed systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2154017)