Naslov
Properties of Time-Sensitive Distributed Systems: Verification and Complexity

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

Vrsta, podvrsta i kategorija rada
Sažeci sa skupova, sažetak, znanstveni

Izvornik
Book of Abstracts LAP 2022 / - Dubrovnik, 2022, 27-28

Skup
Logic and Applications 2022

Mjesto i datum
Dubrovnik, Hrvatska, 26.09.2022. - 29.09.2022

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
Time-Sensitive Distributed Systems, Multiset Rewriting, Complexity

Sažetak
We develop a Multiset Rewriting language with explicit time for the specification and analysis of various properties of Time-Sensitive Distributed Systems (TSDS). In particular, we focus on a class of systems called Progressing Timed Systems (PTS), where intuitively only a finite number of actions can be executed in a bounded time period. Such systems are formalized using explicit time constraints to specify system actions, system goals and properties such as compliance. We consider desirable properties of TSDSes that are specified over sets of traces of system rules with possible interference from the environment. A “good trace” is an infinite trace of system rules in which the goals are satisfied perpetually. We formalize various desirable properties of TSDSes: realizability (there exists a good trace), survivability (where, in addition, all admissible traces are good), recoverability (all compliant traces do not reach points-of-no- return), and reliability (the system can always continue functioning using a good trace). We consider the relations among these properties and their computational complexity. We prove that for this class of systems the properties of recoverability and reliability coincide and are PSPACE-complete. Furthermore, if we impose a bound on time (as in bounded model-checking), we show that for PTS the reliability property is in the Πp2 class of the polynomial hierarchy, a subclass of PSPACE. We also show that the bounded survivability is both NP-hard and coNP-hard.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo

POVEZANOST RADA