Pretražite po imenu i prezimenu autora, mentora, urednika, prevoditelja

Napredna pretraga

Pregled bibliografske jedinice broj: 1159435

On the Complexity of Verification of Time-Sensitive Distributed Systems


Kanovich, Max; Ban Kirigin, Tajana; Nigam, Vivek; Scedrov, Andre; Talcott, Carolyn
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:

Avatar Url Tajana Ban Kirigin (autor)

Poveznice na cjeloviti tekst rada:

doi link.springer.com

Citiraj ovu publikaciju:

Kanovich, Max; Ban Kirigin, Tajana; Nigam, Vivek; Scedrov, Andre; Talcott, Carolyn
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)
Kanovich, M., Ban Kirigin, T., Nigam, V., Scedrov, A. & Talcott, C. (2021) On the Complexity of Verification of Time-Sensitive Distributed Systems. U: Dougherty, D., Meseguer, J., Mödersheim, S. & Rowe, P. (ur.)Protocols, Strands, and Logic. Lecture Notes in Computer Science, vol 13066 doi:10.1007/978-3-030-91631-2_14.
@article{article, author = {Kanovich, Max and Ban Kirigin, Tajana and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn}, year = {2021}, pages = {251-275}, DOI = {10.1007/978-3-030-91631-2\_14}, keywords = {Multiset Rewriting, Time-Sensitive Distributed Systems, Complexity}, doi = {10.1007/978-3-030-91631-2\_14}, isbn = {978-3-030-91631-2}, title = {On the Complexity of Verification of Time-Sensitive Distributed Systems}, keyword = {Multiset Rewriting, Time-Sensitive Distributed Systems, Complexity}, publisher = {Springer}, publisherplace = {Haifa, Izrael} }
@article{article, author = {Kanovich, Max and Ban Kirigin, Tajana and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn}, year = {2021}, pages = {251-275}, DOI = {10.1007/978-3-030-91631-2\_14}, keywords = {Multiset Rewriting, Time-Sensitive Distributed Systems, Complexity}, doi = {10.1007/978-3-030-91631-2\_14}, isbn = {978-3-030-91631-2}, title = {On the Complexity of Verification of Time-Sensitive Distributed Systems}, keyword = {Multiset Rewriting, Time-Sensitive Distributed Systems, Complexity}, publisher = {Springer}, publisherplace = {Haifa, Izrael} }

Časopis indeksira:


  • Scopus


Citati:





    Contrast
    Increase Font
    Decrease Font
    Dyslexic Font