Pregled bibliografske jedinice broj: 1159435
On the Complexity of Verification of Time-Sensitive Distributed Systems
On the Complexity of Verification of Time-Sensitive Distributed Systems // Protocols, Strands, and Logic. Lecture Notes in Computer Science, vol 13066 / Dougherty, Daniel ; Meseguer, José ; Mödersheim, Sebastian Alexander ; Rowe, Paul (ur.).
Haifa, Izrael: Springer, 2021. str. 251-275 doi:10.1007/978-3-030-91631-2_14 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
CROSBI ID: 1159435 Za ispravke kontaktirajte CROSBI podršku putem web obrasca
Naslov
On the Complexity of Verification of Time-Sensitive
Distributed Systems
Autori
Kanovich, Max ; Ban Kirigin, Tajana ; Nigam, Vivek ; Scedrov, Andre ; Talcott, Carolyn
Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni
Izvornik
Protocols, Strands, and Logic. Lecture Notes in Computer Science, vol 13066
/ Dougherty, Daniel ; Meseguer, José ; Mödersheim, Sebastian Alexander ; Rowe, Paul - : Springer, 2021, 251-275
ISBN
978-3-030-91631-2
Skup
Festschrift of Joshua Guttman
Mjesto i datum
Haifa, Izrael, 11.08.2022. - 12.08.2022
Vrsta sudjelovanja
Predavanje
Vrsta recenzije
Međunarodna recenzija
Ključne riječi
Multiset Rewriting ; Time-Sensitive Distributed Systems ; Complexity
Sažetak
This paper develops a Multiset Rewriting language with explicit time for specifying and analyzing Time-Sensitive Distributed Systems (TSDS). Goals of a TSDS must be satisfied by the system perpetually, in spite of a possible environment interference. Goals are often specified using explicit time constraints. A good trace is an infinite trace in which goals are perpetually satisfied. 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 further properties, recoverability (all compliant traces do not reach points-of-no-return) and reliability (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 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 $\Delta_2^p$ class of the polynomial hierarchy.
Izvorni jezik
Engleski
Znanstvena područja
Matematika, Računarstvo
POVEZANOST RADA
Projekti:
HRZZ-UIP-2017-05-9219 - Formalno rasuđivanje i semantike (FORMALS) (Perkov, Tin, HRZZ - 2017-05) ( CroRIS)
Ustanove:
Sveučilište u Rijeci, Fakultet za matematiku
Profili:
Tajana Ban Kirigin
(autor)
Citiraj ovu publikaciju:
Časopis indeksira:
- Scopus