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

Institute of Applied Information Processing and Communications (7050)

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

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.

Original language	English
Title of host publication	Computer Aided Verification
Publisher	Springer
Pages	410-424
ISBN (Print)	978-3-642-14294-9
DOIs	https://doi.org/10.1007/978-3-642-14295-6_36
Publication status	Published - 2010
Event	22nd International Conference on Computer Aided Verification (CAV 2010) - Edinburgh, United Kingdom Duration: 15 Jul 2010 → 19 Jul 2010

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	6174

Conference

Conference	22nd International Conference on Computer Aided Verification (CAV 2010)
Country/Territory	United Kingdom
City	Edinburgh
Period	15/07/10 → 19/07/10

Access to Document

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

GR1.pdfAccepted author manuscript, 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
Project: Research project
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
Project: Research area
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
Project: Research project

Cite this

@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

Publication series

Conference

Access to Document

Fingerprint

Projects

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

Cite this