Bradfield | Verifying Temporal Properties of Systems | Buch | 978-1-4684-6821-2 | sack.de

Buch, Englisch, 116 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 201 g

Reihe: Progress in Theoretical Computer Science

Bradfield

Verifying Temporal Properties of Systems


Softcover Nachdruck of the original 1. Auflage 1992
ISBN: 978-1-4684-6821-2
Verlag: Birkhäuser Boston

Buch, Englisch, 116 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 201 g

Reihe: Progress in Theoretical Computer Science

ISBN: 978-1-4684-6821-2
Verlag: Birkhäuser Boston


This monograph aims to provide a powerful general-purpose proof tech­ nique for the verification of systems, whether finite or infinite. It extends the idea of finite local model-checking, which was introduced by Stirling and Walker: rather than traversing the entire state space of a model, as is done for model-checking in the sense of Emerson, Clarke et ai. (checking whether a (finite) model satisfies a formula), local model-checking asks whether a particular state satisfies a formula, and only explores the nearby states far enough to answer that question. The technique used was a tableau method, constructing a tableau according to the formula and the local structure of the model. This tableau technique is here generalized to the infinite case by considering sets of states, rather than single states; because the logic used, the propositional modal mu-calculus, separates simple modal and boolean connectives from powerful fix-point operators (which make the logic more expressive than many other temporal logics), it is possible to give a rela­ tively straightforward set of rules for constructing a tableau. Much of the subtlety is removed from the tableau itself, and put into a relation on the state space defined by the tableau-the success of the tableau then depends on the well-foundedness of this relation. The generalized tableau technique is exhibited on Petri nets, and various standard notions from net theory are shown to playa part in the use of the technique on nets-in particular, the invariant calculus has a major role.

Bradfield Verifying Temporal Properties of Systems jetzt bestellen!

Zielgruppe


Research


Autoren/Hrsg.


Weitere Infos & Material


1. Introduction.- 1.1 Infinite state model-checking.- 1.2 Background.- 1.3 Local model-checking and infinite systems.- 1.4 Synopsis.- 2. Program Logics and the Mu-Calculus.- 2.1 Semantics of temporal logics.- 2.2 The propositional modal mu-calculus.- 3. The Tableau System.- 3.1 Intuition behind the tableau system.- 3.2 Definition of the tableau system.- 3.3 Simple examples.- 3.4 Soundness of the tableau system.- 3.5 Completeness of the tableau system.- 3.6 Variations on the theme.- 3.7 The tableau system and Hoare logic.- 4. Applications to Nets.- 4.1 Petri nets.- 4.2 Basic application to nets.- 4.3 Using schematic tableaux.- 4.4 Using limited reachability analysis—the coverability graph.- 4.5 Some remarks on compositionality.- 5. The Complexity of Mu-Formulae on Nets.- 5.1 Beyond semi-linearity.- 5.2 Undecidability of the model-checking problem.- 5.3 Ascending the arithmetical hierarchy.- 5.4 Beyond the arithmetical hierarchy.- 6. Conclusions and Further Work.- 6.1 Incorporating reasoning.- 6.2 Decidability of model-checking.- 6.3 Proving success.- References.- List of Notations.



Ihre Fragen, Wünsche oder Anmerkungen
Vorname*
Nachname*
Ihre E-Mail-Adresse*
Kundennr.
Ihre Nachricht*
Lediglich mit * gekennzeichnete Felder sind Pflichtfelder.
Wenn Sie die im Kontaktformular eingegebenen Daten durch Klick auf den nachfolgenden Button übersenden, erklären Sie sich damit einverstanden, dass wir Ihr Angaben für die Beantwortung Ihrer Anfrage verwenden. Selbstverständlich werden Ihre Daten vertraulich behandelt und nicht an Dritte weitergegeben. Sie können der Verwendung Ihrer Daten jederzeit widersprechen. Das Datenhandling bei Sack Fachmedien erklären wir Ihnen in unserer Datenschutzerklärung.