Wojciech Penczek, Agata Półrola Advances in Verification of Time Petri Nets and Timed Automata Studies in Computational Intelligence, Volume 20 Editor-in-chief Prof. Janusz Kacprzyk Systems Research Institute Polish Academy of Sciences ul. Newelska 6 01-447 Warsaw Poland E-mail: [email protected] Further volumes of this series Vol. 12. Jonathan Lawry can be found on our homepage: Modelling and Reasoning with Vague Con- springer.com cepts, 2006 ISBN 0-387-29056-7 Vol. 5. Da Ruan, Guoqing Chen, Etienne E. Vol. 13. Nadia Nedjah, Ajith Abraham, Kerre, Geert Wets (Eds.) Luiza de Macedo Mourelle (Eds.) Intelligent Data Mining, 2005 Genetic Systems Programming, 2006 ISBN 3-540-26256-3 ISBN 3-540-29849-5 Vol. 6. Tsau Young Lin, Setsuo Ohsuga, Vol. 14. Spiros Sirmakessis (Ed.) Churn-Jung Liau, Xiaohua Hu, Shusaku Adaptive and Personalized Semantic Web, Tsumoto (Eds.) 2006 Foundations of Data Mining and Knowledge ISBN 3-540-30605-6 Discovery, 2005 ISBN 3-540-26257-1 Vol. 15. Lei Zhi Chen, Sing Kiong Nguang, Xiao Dong Chen Vol. 7. Bruno Apolloni, Ashish Ghosh, Ferda Modelling and Optimization of Alpaslan, Lakhmi C. Jain, Srikanta Patnaik Biotechnological Processes, 2006 (Eds.) ISBN 3-540-30634-X Machine Learning and Robot Perception, 2005 Vol. 16. Yaochu Jin (Ed.) ISBN 3-540-26549-X Multi-Objective Machine Learning, 2006 ISBN 3-540-30676-5 Vol. 8. Srikanta Patnaik, Lakhmi C. Jain, Spyros G. Tzafestas, Germano Resconi, Vol. 17. Te-Ming Huang, Vojislav Kecman, Amit Konar (Eds.) Ivica Kopriva Innovations in Robot Mobility and Control, Kernel Based Algorithms for Mining Huge 2005 Data Sets, 2006 ISBN 3-540-26892-8 ISBN 3-540-31681-7 Vol. 9. Tsau Young Lin, Setsuo Ohsuga, Vol. 18. Chang Wook Ahn Churn-Jung Liau, Xiaohua Hu (Eds.) Advances in Evolutionary Algorithms, 2006 Foundations and Novel Approaches in Data ISBN 3-540-31758-9 Mining, 2005 ISBN 3-540-28315-3 Vol. 19. Ajita Ichalkaranje, Nikhil Ichalkaranje, Lakhmi C. Jain (Eds.) Vol. 10. Andrzej P. Wierzbicki, Yoshiteru Intelligent Paradigms for Assistive and Nakamori Preventive Healthcare, 2006 Creative Space, 2005 ISBN 3-540-31762-7 ISBN 3-540-28458-3 Vol. 20. Wojciech Penczek, Agata Półrola Vol. 11. Antoni Ligęza Advances in Verification of Time Petri Nets Logical Foundations for Rule-Based and Timed Automata, 2006 Systems, 2006 ISBN 3-540-32869-6 ISBN 3-540-29117-2 Wojciech Penczek Agata Półrola Advances in Verification of Time Petri Nets and Timed Automata A Temporal Logic Approach With 124 Figures ABC Doc. dr. hab. Wojciech Penczek Dr. Agata Półrola Institute of Computer Science Faculty of Mathematics Polish Academy of Sciences University of Łódz ul. Ordona 21 ul. Banacha 22 01-237 Warsaw 90-238 Łódz Poland Poland and E-mail: [email protected] Institute of Informatics Podlasie Academy ul. Sienkiewicza 51 08-110 Siedlce Poland E-mail: [email protected] Library of Congress Control Number: 2006925476 ISSN print edition: 1860-949X ISSN electronic edition: 1860-9503 ISBN-10 3-540-32869-6 Springer Berlin Heidelberg New York ISBN-13 978-3-540-32869-8 Springer Berlin Heidelberg New York This work is subject to copyright. All rights are reserved, whether the whole or part of the mate- rial is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recita- tion, broadcasting, reproduction on microfilm or in any other way, and storage in data banks. Duplication of this publication or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965, in its current version, and permission for use must always be obtained from Springer-Verlag. Violations are liable to prosecution under the German Copyright Law. Springer is a part of Springer Science+Business Media springer.com © Springer-Verlag Berlin Heidelberg 2006 Printed in the Netherlands The use of general descriptive names, registered names, trademarks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. Cover design: deblik, Berlin Typesetting by the authors and SPI Publisher Services Printed on acid-free paper SPIN: 11599357 89/SPI 5 4 3 2 1 0 To our families Introduction Verification of real-time systems is an important subject of research. This is highly motivated by an increasing demand to verify safety critical systems, i.e.,time-dependentdistributedsystems,failureofwhichcouldcausedramatic consequences for both people and hardware. Temporallogicmethodshavebeenusedforverificationoverthelasttwenty years, proving their usefulness for such an application. Whereas infinite state systemsstillrequiredeductiveproofmethods,systemsoffiniteabstractmod- els can be verified using algorithmic approaches. This means that the veri- fication process can be fully automated. One of the most promising sets of techniques forverification isknown asmodel checking. Essentially, inthisfor- malism verifying that a property follows from a system specification amounts tocheckingwhetherornotatemporalformulaisvalidonamodelrepresenting all the possible computations of the system. Several models of real-time systems are usually considered in the litera- ture, but timed automata (TA) [10] and time Petri nets (TPNs) [106] be- long to the most widely used. For these models, one is, usually, interested in checking reachability or more involved temporal properties that are typically ∗ expressed either in a standard temporal logic like LTL and CTL , or in a timed extension of CTL, called TCTL [7]. Unfortunately, practical applica- bility of model checking methods is strongly limited by the state explosion problem, which makes models grow exponentially in the number of the con- current processes of a system. For real-time systems, this problem occurs with a particular strength, which follows from infinity of the dense time do- main. Therefore, existing verification techniques frequently apply symbolic representations of state spaces using either operations on Difference Bound Matrices[68]orsimilarstructures[32]forrepresentingstatesofabstractmod- els, or variations of Boolean Decision Diagrams like Clock Decision Diagrams (CDDs) [24,166], Numeric Decision Diagrams (NDDs) [18], Difference Deci- sionDiagrams(DDDs)[107,108],orClockRestrictionDiagrams(CRDs)[168]. Quite recently, a new approach to verification of real time systems, based on SAT-related algorithms, has been suggested. The reason for this is a dra- VIII Introduction matic increase in efficiency of SAT-solvers over the last few years. The SAT- based approach can exploit either a sequence of translations starting from a timed system and a timed temporal property, going via (quantified) sep- aration logic to quantified propositional logic and further to propositional logic [20,110,140] or a direct translation from a timed system and a timed temporal property to propositional logic [120,171,177]. Finitestatemodelsfortimedsystems,preservingpropertiestobechecked, are usually built using the detailed region graph approach or (possibly mini- mal) abstract models, based on state classes or regions. Algorithms for gen- erating such models have been defined for time Petri nets [32,35,73,102,111, 117,163,174], as well as for timed automata [7,8,41,66,125,159]. Itseemsthatinspiteofthesameunderlyingtimedstructure,modelcheck- ing methods for time Petri nets and timed automata have been developed independently of each other. However, several attempts to combine the two approaches were made, concerning both a structural translation of one model into the other [52,60,78,89,103,124,144] or an adaptation of existing verifi- cation techniques [73,111,163]. The aim of this monograph is to present a recent progress in the devel- opment of two model checking methods, based on either building abstract state spaces or application of SAT-based symbolic techniques. The latter is achieved indirectly for time Petri nets, namely via a translation to timed au- tomata.Ourspecialemphasisisputnotonlyontheverificationmethods,but also on specification languages and their semantics. Structure of the book Chapter 1ofthisbookintroducesPetrinets,discussestheirtimeextensions, andprovidesadefinitionoftimePetrinets.Ourattentionisfocusedonaspe- cial kind of TPNs – distributed time Petri nets, which, in a sense, correspond to networks of timed automata introduced in Chapter 2. Two main alterna- tive approaches to the semantics of time Petri nets are considered. The first of them consists in assigning clocks to various components of the net, i.e., the transitions, the places, or the processes, whereas the second exploits the so-called firing intervals of the transitions. The chapter ends with comparing the above semantics as well as their dense and discrete versions. Chapter 2 considers timed automata, which were introduced by Alur andDill[10].Timedautomataareextensionsoffinitestateautomata.Wegive semanticsoftimedautomataandshowhowtodefinetheirproduct.Typically, we consider networks of timed automata, consisting of several concurrent TA running in parallel and communicating with each other. Concrete models are defined and progressiveness is discussed. Chapter 3 deals with various structural translations from TPNs to TA. Theyenableanapplicationofspecificverificationmethodsfortimedautomata to time Petri nets. Several methods of translating time Petri nets to timed automata have been already developed. However, in most cases translations Introduction IX produce automata which extend timed automata. We sketch some of the ex- istingapproaches,butfocusmainlyonthetranslationsthatcorrespondtothe semantics of time Petri nets, associating clocks with various components of the nets, like the places, the transitions, or the processes. Chapter 4introducestemporalspecificationlanguages.Westartourpre- ∗ sentationwiththestandardbranchingtimelogicCTL ,itsextensionmodalµ- calculus,andthendiscusstimedtemporallogics:TCTLandtimedµ-calculus. It is important to mention that we consider two versions of syntax of TCTL interpreted over either weakly or strongly monotonic runs. Chapter 5 gives model abstraction methods based on state classes ap- proaches for TPNs and on partition refinement for TA. For time Petri nets we discuss different abstract models like state class graphs, geometric re- gion graphs, atomic state class graphs, pseudo-atomic state class graphs, and strong state class graphs. For timed automata we concentrate on detailed re- gion graphs, (pseudo-)bisimulating models, (pseudo-)simulating models, and forward-reachabilitygraphs.Thelastsectionofthischaptergivesanoverview of difference bound matrices (DBMs), which are used for representing states of abstract models. Chapter 6 deals with model checking methods for CTL. These methods include a standard state labelling algorithm as well as an automata-theoretic approach. Moreover, we show that model checking for TCTL over timed au- tomata can be reduced to model checking for CTL. Chapter 7 discusses SAT-based verification techniques, like bounded (BMC) and unbounded model checking (UMC). The main idea behind BMC [120,171]consistsintranslatingthemodelcheckingproblemforanexistential fragment of some branching-time temporal logic (like CTL or TCTL) on a fraction of a model into a test of propositional satisfiability, for which refined toolsalreadyexist[109].UnlikeBMC,UMC[105,140]dealswithunrestricted temporal logics checked on complete models at the price of a decrease in efficiency. Each chapter of our book is accompanied with pointers to the literature, where descriptions of complementary methods or formalisms can be found. Acknowledgement. The authors would like to thank the following people for com- mentingonthismonograph:BernardBerthomieu,FranckCassez,PiotrDembin´ski, Magdalena Kacprzak, S(cid:1)lawomir Lasota, Oded Maler, Olivier H. Roux, Maciej Szreter,StavrosTripakis,Boz˙ena Wo´zna,TomohiroYonedaandAndrzejZbrzezny. Allthecommentsfromtheaboveexpertshavegreatlyhelpedtoimprovethebook. TheauthorsacknowledgesupportfromMinistryofScienceandEducation(grant No. 3T11C 011 28). Warsaw, Poland, Wojciech Penczek December 2005 Agata P´o(cid:1)lrola Contents List of Figures.................................................XV List of Symbols ................................................XXI Part I Specifying Timed Systems and Their Properties 1 Petri Nets with Time...................................... 3 1.1 Incorporating Time into Petri Nets ........................ 6 1.2 Time Petri Nets......................................... 7 1.2.1 Distributed Time Petri Nets ........................ 8 1.2.2 Semantics: The Clock Approach..................... 11 Clocks Assigned to the Transitions .................. 11 Clocks Assigned to the Places....................... 12 Clocks Assigned to the Processes .................... 14 1.2.3 Semantics: Firing Intervals ......................... 15 1.3 Reasoning about Time Petri Nets.......................... 17 1.3.1 Comparison of the Semantics ....................... 17 1.3.2 Dense versus Discrete Semantics .................... 18 Alternative (Discrete) Semantics .................... 21 1.3.3 Concrete Models for TPNs ......................... 23 1.3.4 Progressiveness in Time Petri Nets .................. 23 1.3.5 The Case of “General” TPNs ....................... 27 2 Timed Automata .......................................... 29 2.1 Time Zones............................................. 29 2.2 Networks of Timed Automata............................. 33 2.3 Semantics of Timed Automata ............................ 38 2.3.1 Alternative (Discrete) Semantics .................... 40 2.4 Concrete Models for TA.................................. 41 2.5 Checking Progressiveness ................................. 42 XII Contents 2.5.1 A Static Technique ................................ 44 2.5.2 Applying Verification Methods ...................... 46 2.5.3 A Solution for Strongly Monotonic Semantics ......... 48 3 From Time Petri Nets to Timed Automata ................ 51 3.1 Translations to Extended Timed Automata ................. 51 3.2 Translation for “Clocks Assigned to the Transitions”......... 53 3.3 Translation for “Clocks Assigned to the Places” ............. 55 3.3.1 Supplementary Algorithms ......................... 57 Obtaining General TA ............................. 57 Obtaining Diagonal-Free TA ........................ 58 3.4 Translation for Distributed Nets........................... 59 3.5 Comparing Expressiveness of TPNs and TA ................ 62 4 Main Formalisms for Expressing Temporal Properties ..... 63 4.1 Non-temporal Logics..................................... 63 4.1.1 Propositional Logic (PL) ........................... 63 Syntax of PL ..................................... 63 Semantics of PL................................... 64 4.1.2 Quantified Propositional Logic (QPL)................ 65 Syntax of QPL.................................... 65 Semantics of QPL ................................. 65 4.1.3 (Quantified) Separation Logic ((Q)SL) ............... 65 Syntax of (Q)SL .................................. 65 Semantics of (Q)SL................................ 66 4.2 Untimed Temporal Logics ................................ 66 ∗ 4.2.1 Computation Tree Logic* (CTL ) ................... 67 ∗ Syntax of CTL ................................... 67 ∗ Sublogics of CTL ................................. 67 ∗ Semantics of CTL ................................ 69 4.2.2 Modal µ-Calculus ................................. 71 Syntax of Modal µ-Calculus ........................ 71 Semantics of Modal µ-Calculus...................... 72 4.2.3 InterpretationofTemporalLogicsoverTimedSystems Models........................................... 74 4.3 Timed Temporal Logics .................................. 75 4.3.1 Timed Computation Tree Logic (TCTL) ............. 75 Syntax of TCTL .................................. 75 Semantics of TCTL over Timed Systems ............. 76 Strongly Monotonic Interval Semantics ...... 76 Weakly Monotonic Interval Semantics ....... 78 4.3.2 Timed µ-Calculus (Tµ)............................. 80 Syntax of Tµ...................................... 80 Semantics of Tµ ................................... 80 4.3.3 Syntax and Semantics of TCTLC .................... 82