Advances in Verification of Time Petri Nets and Timed Automata :
[Book]
a Temporal Logic Approach
by Wojciech Penczek, Agata Pólrola.
Berlin, Heidelberg
Springer-Verlag Berlin Heidelberg
2006
Studies in Computational Intelligence, 20.
Titre de l'écran-titre (visionné le 2 juillet 2008).
Cover --;Contents --;List of Figures --;List of Symbols --;Part I: Specifying Timed Systems and Their Properties --;CH 1 Petri Nets with Time --;1.1 Incorporating Time into Petri Nets --;1.2 Time Petri Nets --;1.3 Reasoning about Time Petri Nets --;CH 2 Timed Automata --;2.1 Time Zones --;2.2 Networks of Timed Automata --;2.3 Semantics of Timed Automata --;2.4 Concrete Models for TA --;2.5 Checking Progressiveness --;CH 3 From Time Petri Nets to Timed Automata --;3.1 Translations to Extended Timed Automata --;3.2 Translation for "Clocks Assigned to the Transitions" --;3.3 Translation for "Clocks Assigned to the Places" --;3.4 Translation for Distributed Nets --;3.5 Comparing Expressiveness of TPNs and TA --;CH 4 Main Formalisms for Expressing Temporal Properties --;4.1 Non-temporal Logics --;4.2 Untimed Temporal Logics --;4.3 Timed Temporal Logics --;Part II: Model Generation and Verification --;CH 5 Abstract Models --;5.1 Model Generation for Time Petri Nets --;5.2 Model Generation for Timed Automata --;5.3 Difference Bounds Matrices --;CH 6 Explicit Verification --;6.1 Model Checking for CTL --;6.2 Model Checking for TCTL over Timed Automata --;6.3 Selected Tools --;CH 7 Verification Based on Satisflability Checking --;7.1 Bounded Model Checking Using Direct Translation to SAT --;7.2 Bounded Model Checking via Translation to SL --;7.3 Unbounded Model Checking for T --;7.4 Deciding Separation Logic (MATH-SAT) --;7.5 Deciding Propositional Formulas (SAT) --;7.6 From a Fragment of QPL to PL --;7.7 Remaining Symbolic Approaches --;Overview --;7.8 Selected Tools --;Concluding Remarks and Future Research Directions --;References --;Index --;Author Index --;Last Page.