Robustness in the Presence of Liveness

Roderick Paul Bloem; Krishnendu Chatterjee; Karin Greimel; Thomas Henzinger; Barbara Jobstmann

doi:10.1007/978-3-642-14295-6_36

Robustness in the Presence of Liveness

Roderick Paul Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas Henzinger, Barbara Jobstmann

Institut für Angewandte Informationsverarbeitung und Kommunikationstechnologie (7050)

Publikation: Beitrag in Buch/Bericht/Konferenzband › Beitrag in einem Konferenzband › Begutachtung

Abstract

Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which prescribes, for any number of environment assumptions that are violated, a minimal number of system guarantees that must still be fulfilled. This notion of robustness can be formulated and realized using a Generalized Reactivity formula. We present an algorithm for synthesizing robust systems from such formulas. For the important special case of Generalized Reactivity formulas of rank 1, our algorithm improves the complexity of [PPS06] for large specifications with a small number of assumptions and guarantees.

Originalsprache	englisch
Titel	Computer Aided Verification
Herausgeber (Verlag)	Springer
Seiten	410-424
ISBN (Print)	978-3-642-14294-9
DOIs	https://doi.org/10.1007/978-3-642-14295-6_36
Publikationsstatus	Veröffentlicht - 2010
Veranstaltung	22nd International Conference on Computer Aided Verification (CAV 2010) - Edinburgh, Großbritannien / Vereinigtes Königreich Dauer: 15 Juli 2010 → 19 Juli 2010

Publikationsreihe

Name	Lecture Notes in Computer Science
Herausgeber (Verlag)	Springer
Band	6174

Konferenz

Konferenz	22nd International Conference on Computer Aided Verification (CAV 2010)
Land/Gebiet	Großbritannien / Vereinigtes Königreich
Ort	Edinburgh
Zeitraum	15/07/10 → 19/07/10

Zugriff auf Dokument

10.1007/978-3-642-14295-6_36

GR1.pdfAkzeptiertes Autorenmanuskript, 208 KB

EU - DIAMOND - Diagnosis, Error Modelling and Correction for Reliable Systems Design
Khalimov, A., Greimel, K., Jacobs, S., Hofferek, G., Könighofer, B., Könighofer, R. & Bloem, R.
1/01/10 → 31/12/12
Projekt: Forschungsprojekt
Formal Methods for Design & Verification
Jacobs, S., Bloem, R., Könighofer, R., Könighofer, B., Khalimov, A., Hofferek, G. & Braud-Santoni, N.
1/02/08 → 15/07/19
Projekt: Arbeitsgebiet
EU - COCONUT - A correct-by-construction workbench for design and verification of embedded systems
Könighofer, R., Hofferek, G., Greimel, K. & Bloem, R.
1/01/08 → 30/06/10
Projekt: Forschungsprojekt

Dieses zitieren

Bloem, RP, Chatterjee, K, Greimel, K, Henzinger, T & Jobstmann, B 2010, Robustness in the Presence of Liveness. in Computer Aided Verification. Lecture Notes in Computer Science, Bd. 6174, Springer, S. 410-424, 22nd International Conference on Computer Aided Verification (CAV 2010), Edinburgh, Großbritannien / Vereinigtes Königreich, 15/07/10. https://doi.org/10.1007/978-3-642-14295-6_36

@inproceedings{398cf60f1cdb4776a33cf46fc138addc,

title = "Robustness in the Presence of Liveness",

abstract = "Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which prescribes, for any number of environment assumptions that are violated, a minimal number of system guarantees that must still be fulfilled. This notion of robustness can be formulated and realized using a Generalized Reactivity formula. We present an algorithm for synthesizing robust systems from such formulas. For the important special case of Generalized Reactivity formulas of rank 1, our algorithm improves the complexity of [PPS06] for large specifications with a small number of assumptions and guarantees.",

author = "Bloem, {Roderick Paul} and Krishnendu Chatterjee and Karin Greimel and Thomas Henzinger and Barbara Jobstmann",

year = "2010",

doi = "10.1007/978-3-642-14295-6_36",

language = "English",

isbn = "978-3-642-14294-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "410--424",

booktitle = "Computer Aided Verification",

note = "22nd International Conference on Computer Aided Verification (CAV 2010) ; Conference date: 15-07-2010 Through 19-07-2010",

}

TY - GEN

T1 - Robustness in the Presence of Liveness

AU - Bloem, Roderick Paul

AU - Chatterjee, Krishnendu

AU - Greimel, Karin

AU - Henzinger, Thomas

AU - Jobstmann, Barbara

PY - 2010

Y1 - 2010

N2 - Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which prescribes, for any number of environment assumptions that are violated, a minimal number of system guarantees that must still be fulfilled. This notion of robustness can be formulated and realized using a Generalized Reactivity formula. We present an algorithm for synthesizing robust systems from such formulas. For the important special case of Generalized Reactivity formulas of rank 1, our algorithm improves the complexity of [PPS06] for large specifications with a small number of assumptions and guarantees.

AB - Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which prescribes, for any number of environment assumptions that are violated, a minimal number of system guarantees that must still be fulfilled. This notion of robustness can be formulated and realized using a Generalized Reactivity formula. We present an algorithm for synthesizing robust systems from such formulas. For the important special case of Generalized Reactivity formulas of rank 1, our algorithm improves the complexity of [PPS06] for large specifications with a small number of assumptions and guarantees.

U2 - 10.1007/978-3-642-14295-6_36

DO - 10.1007/978-3-642-14295-6_36

M3 - Conference paper

SN - 978-3-642-14294-9

T3 - Lecture Notes in Computer Science

SP - 410

EP - 424

BT - Computer Aided Verification

PB - Springer

T2 - 22nd International Conference on Computer Aided Verification (CAV 2010)

Y2 - 15 July 2010 through 19 July 2010

ER -

Robustness in the Presence of Liveness

Abstract

Publikationsreihe

Konferenz

Zugriff auf Dokument

Fingerprint

Projekte

EU - DIAMOND - Diagnosis, Error Modelling and Correction for Reliable Systems Design

Formal Methods for Design & Verification

EU - COCONUT - A correct-by-construction workbench for design and verification of embedded systems

Dieses zitieren