On the complexity of verification of time-sensitive distributed systems

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

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

Publication date 13 July 2022

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

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)

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.

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

Cites work

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

Cited in

(6)

• Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
• A semantic model for interacting cyber-physical systems
• On the complexity of verifying concurrent transition systems
• Multi-scale verification of distributed synchronisation
• scientific article; zbMATH DE number 1533829 (Why is no real title available?)
• 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)