^XISIKpn Masaryk University, Brno Faculty of Informatics On Extensions of Process Rewrite Systems Vojtěch Řehák PhD Thesis 2007 Abstract The thesis studies properties of Process Rewrite Systems (PRS) and their extensions. Namely, it introduces an extension of PRS, so called weakly extended Process Rewrite Systems (wPRS). This work compares the expressiveness of wPRS with original PRS classes and their known extensions. In addition, it studies decidability of problems related to model checking and other formal verification procedures such as weak and strong bisimulation, the reachability problem, etc. We aim to extend expressive power of known modelling facilities while preserving decidability and maintaining reasonable complexity bounds for problems related to (automatic) verification. Disertační práce je zaměřena na vlastnosti procesových přepisovacích systémů (PRS) a jejich rozšíření. Práce představuje nové rozšíření hierarchie procesových přepisovacích systémů o slabou konečně stavovou jednotkou (wPRS) a porovnává vyjadřovací sílu těchto tříd s dosud známými rozšířeními. Dále práce studuje hranice rozhodnutelnosti zajímavých problémů vztahujících se k ověřování vlastností modelů, či jiným metodám formální verifikace. Ze zajímavých problémů jmenujme například problém dosažitelnosti, či problémy rozhodování silné a slabé bisimulace. Cílem práce je rozšířit vyjadřovací sílu známých modelů o přirozeně motivované možnosti, které však v rozumné míře zachovají rozhodnutel-nost zmiňovaných problémů a složitostní odhady algoritmů řešících tyto problémy. Acknowledgements First of all I would like to thank my supervisor Mojmír Křetínský for his help, encouragement, collaboration, and many valuable and wide-ranging discussions during my studies. I am grateful to him also for careful reading a draft of this thesis. I would like to thank Jan Strejček for his constant support and exemplary collaboration. I thank Laura Bozzelli for her collaboration on some LTL model checking problems. I also very much appreciate the collaboration with David Šafránek and David Antoš. I would like to express my gratitude to Antonín Kučera, Jiří Srba, Hans Hüttel, and Luca Aceto for valuable suggestions, comments, and pointers. My thanks go to the members of Parallel and Distributed Systems Laboratory (ParaDiSe) and to the members of Institute for Theoretical Computer Science (ITI). I especially thank Jan Obržálek for his consultation regarding my English. Finally, I would like to thank my wife Kateřina and my parents for their love, support, and patience. Vojtěch Řehák Contents 1 Introduction 1 1.1 Subject of This Thesis....................... 2 1.2 Thesis Organisation and Contribution............. 3 1.3 Author's Publications ...................... 5 2 Process Rewrite Systems (PRS) 9 2.1 Basic Definitions.......................... 9 2.2 Definition of Process Rewrite Systems............. 12 2.3 Hierarchy of Process Rewrite Systems............. 14 3 State Extended PRS (sePRS) 19 3.1 Definition of State Extended PRS................ 19 3.2 Hierarchy of State Extended PRS................ 20 3.2.1 PN C sePA........................ 22 3.2.2 Strictness and Incomparability............. 26 4 PRS with Finite Constraint Systems (fcPRS) 31 4.1 Definition of PRS with Finite Constraint Systems....... 31 4.2 Hierarchy of PRS with Finite Constraint Systems....... 34 5 Weakly Extended PRS (wPRS) 41 5.1 Definition of Weakly Extended PRS............... 41 5.2 Hierarchy of Weakly Extended PRS............... 43 5.2.1 wBPP Non-bisimilar to any fcPAD........... 46 5.2.2 PPDA Non-bisimilar to any wPAD........... 48 5.2.3 wBPA Non-bisimilar to any fcPAN........... 49 5.2.4 PDA Non-bisimilar to any wPAN ........... 57 5.2.5 Intuition and Conjectures................ 58 6 Strong Bisimulation Equivalence 61 6.1 Motivation............................. 61 6.2 Definition of Strong Bisimilarity................. 62 6.3 Summary.............................. 62 viii CONTENTS 7 Weak Bisimulation Equivalence 65 7.1 Motivation............................. 65 7.2 Definition of Weak Bisimilarity................. 66 7.3 Undecidability of Weak Bisimilarity.............. 67 7.3.1 wBPA............................ 67 7.3.2 wBPP............................ 68 7.4 Weak Bisimilarity for More Restricted Classes......... 73 7.4.1 NormedfcBPP ...................... 73 7.4.2 NormedfcBPA...................... 74 7.5 Conclusion............................. 77 8 Reachability Problem 81 8.1 Motivation............................. 81 8.2 Reachability Problem for wPRS................. 82 8.3 Applications............................ 87 8.3.1 Model Checking Some Safety Properties........ 87 8.3.2 Semi-decidability of Weak Trace Non-equivalence . . 88 8.3.3 Other Applications.................... 90 8.4 Conclusion............................. 90 9 Branching Time Logics 93 9.1 Motivation............................. 93 9.2 Logics and Studied Problems.................. 94 9.3 Reachability HM Property.................... 97 9.4 Corollaries and Remarks..................... 101 9.5 Evitability Simple Property for Deterministic BPP...... 103 9.6 Summary.............................. 104 9.7 Conclusion............................. 105 10 Linear Time Logic 109 10.1 Motivation............................. 109 10.2 Definitions of the Studied Problems .............. Ill 10.3 Fragment A and Translation of LTL(FS, Gs) into A....... 117 10.4 Model Checking of wPRS against Negated A......... 120 10.5 Model Checking LTL(FS, Ps) ................... 131 10.6 Undecidability Results...................... 140 10.7 Summary.............................. 143 10.8 Conclusion............................. 146 11 LTLdet Model Checking 149 11.1 Motivation............................. 149 11.2 Definition of the Studied Problem................ 150 11.3 Proof Construction........................ 151 11.4 Summary.............................. 155 CONTENTS______________________________________________________ix 12 Conclusion and Future Work 157 Bibliography 159 Chapter 1 Introduction The need for formal modelling of systems and subsequent more or less automatic verification is indisputable. There have been many words written about model checking [CGP99] being a suitable automatic method for model verification. When choosing a modelling formalism we need to have in mind two features going against each other. On the one hand, we want such a formalism to be expressive enough to model as much system behaviour as possible. This is the most important parameter for users of a modelling/verification tool. On the other hand, the more powerful the formalism is, the more complex verification algorithms are. Basic model checking algorithms are based on exhaustive searching of a system state space. As the state space is usually huge, this approach leads to large computational requirements. A significant advancement was achieved by so called symbolic approach [McM93] that was successfully applied to hardware design verification. Unfortunately, the symbolic model checking did not achieve such great success in case of software verification. Currently, several interesting approaches are investigated in order to improve the applicability of model checking. The most useful technique is an application of abstraction to reduce the size of state space of the model. There are two basic approaches to abstraction, over-approximation and under-approximation. Over-approximation can possibly introduce new behaviour to the model, while under-approximation can possibly remove some valid behaviour of the modelled system. Hence, an over-approximation approach is suitable for proving correctness, since correctness of the abstract model implies correctness of the original system. On the other hand, an under-approximation approach works very well for bug hunting, as every incorrect behaviour in the abstract model has some, also incorrect, counterpart in the original system. Even though software systems are usually of a finite size, they can be parametrised. The parameter can be maximal stack size, number of pro- 2 INTRODUCTION cesses running in parallel, etc. This quite naturally suggests to abstract away from these parameters and instead consider an infinite state system that is an over-approximation of the original one. In that case the state space increases its size, but the system can get more regular structure. Therefore focusing on the structure, rather than state by state exploration of the whole state space, can bring considerable improvement. The crucial difference follows from the fact that in such an abstract system the complexity of model checking depends on the size of the specification rather than on the size of the state space. 1.1 Subject of This Thesis PRS In this thesis we focus on infinite state structures defined by a finite number of rules, which in turn induce an infinite transition relation of the system. We use the concept of Process Rewrite Systems (PRS) introduced by Mayr in his PhD thesis [May98]. Process rewrite systems are an elegant and unified approach that subsumes many of the important infinite state formalisms studied before, for example Petri nets (PN), pushdown automata (PDA), and various process algebras (BPA, BPP, PA). Process rewrite systems form a strict hierarchy with respect to strong bisimulation equivalence. This hierarchy is called the PRS-hierarchy. It is worth mentioning that the PRS-hierarchy subsumes hierarchies of infinite systems defined by Stirling, Caucal, and Moller [Cau92, Mol98]. sePRS It is well known that PA can model both parallel and sequential processes but without any communication among them. Let us mention that even the most general class of the PRS-hierarchy does not support an arbitrary kind of communication between processes. Some kind of global control is a very natural and useful instrument from the model designer point of view. Let us mention the success of PDA in modelling recursive programs or of PN in modelling dynamic creation of concurrent processes. In both these formalisms we have a notion of a finite-state control unit (FSU) which can keep global information and thus provide means of communication between modelled recursive programs or concurrent processes. Process rewrite systems extended with an FSU, called state-extended PRS, first appeared in [JKM01]. Unfortunately, using an FSU to extend the PRS rewriting mechanism is too powerful, since the reachability problem becomes undecidable even for a state extended version of PA processes (sePA) [BEH95]. fcPRS In [Str02], Strejček transferred some principles of Concurrent Constraint Programming (CCP) [SR90] to the formalism of process rewrite systems. The mechanism of rewrite systems is extended with a very restricted form of finite state unit. The unit behaves as a shared CCP store which is seen as a constraint on the values that common variables can represent. Strejček 1.2 THESIS ORGANISATION AND CONTRIBUTION 3 has also shown that his definition of PRS with finite constraint systems (fcPRS) brings new classes lying strictly (with respect to strong bisimula-tion) between each original PRS class and its non-equivalent state extended counterpart - with one exception of PRS/sePRS, where the situation is not clear. Unfortunately the finite constraint specification is quite complicated and so it is unhandy for modelling systems of processes. More precisely it remains "too close" to its initial motivation (coming from CCP) to be useful for modelling different kind of FSU. In this thesis we introduce yet another extension lying between the fi- wPRS nite constraint extension and the state extension. A definition of our extension is very close to the state extension and at the same time it keeps advantages of the less expressive classes (esp. decidability of the reachability problem). We define weakly extended PRS (wPRS) classes where the FSU is subject to some restrictions inspired by weak finite automata introduced in [MSS92]. (Here we use a nondeterministic automata rather than alternating ones.) Roughly speaking, weakly extended PRS formalism is a state extended PRS where the FSU contains no cycles except self loops; in other words, the state of FSU changes only finitely many times during an execution. Weakly extended PRS formalism proves to be a very good compromise standing in between very expressible, but Turing powerful, sePRS and non-extended PRS lacking the advantage of global communication. Hence, this formalism provides the best comfort to system designers while still preserving some algorithmic verification abilities essential for developers of a potential verification tool. Moreover, the weak extension makes it easy to come up with some of the constructive proofs. It is worth mentioning that some of these proofs bring new results also for the non-extended PRS classes. 1.2 Thesis Organisation and Contribution Besides introducing weakly extended PRS itself, we have proved the strictness of an extended PRS-hierarchy with respect to strong bisimulation equivalence. The extended PRS-hierarchy consists of all PRS, fcPRS, wPRS, and sePRS classes. The following four chapters are devoted to these (extended) PRS formalisms. Each chapter defines one of the formalisms and includes results proving strictness of the relations between the classes introduced so far. The results are published in [May98], [Str02], and our papers [KRS04b] and [KRS04a]. Some of the strictness problems are still open. In these cases we provide our conjectures supported by intuitive explanations only — see "Intuition and Conjectures" parts of Chapter 3,4, and 5. In the remaining chapters we focus on some interesting problems related to model checking and other formal verification procedures such 4 INTRODUCTION as weak and strong bisimulation checking. Chapter 6 reviews (un)decid-ability as well as complexity boundaries of strong bisimilarity between two states of a given extended PRS. As we have not reached any new results, this chapter only summarises all known results in this area. Chapter 7 studies a weak bisimilarity problem. After a listing of all known results, we show our results of [KRS06] stating that the problem is undecidable for weakly extended versions of BPA and BPP. We also strengthen the result by proving that the weak bisimilarity problem is undecidable even for normed subclasses of BPA and BPP extended with finite constraint systems. A reachability problem (i.e. given two states a,ß, the problem is whether the state ß is reachable by some computation starting in the state a) can be considered as a basis for all model checking problems. In Chapter 8 we show that the reachability problem remains decidable for the class of wPRS and thus we determine the decidability borderline of the reachability problem in whole extended PRS-hierarchy This result was published in [KRS04a]. Chapter 9 is concentrated on the model checking problem for branching time logics. We deal with model checking for some simple branching time logics, namely EF and EG, and their fragments. We examine the problem whether a given weakly extended process rewrite system (wPRS) contains a reachable state satisfying a given formula of Hennessy-Milner logic. The main result of this chapter is that this problem is decidable. As a corollary we observe that also the problem of strong bisimilarity between wPRS and finite-state systems is decidable. Decidability of the same problem for wPRS subclasses, namely PAN and PRS, has been formulated as an open question. This chapter incorporates our contribution published in [KRS05]. The model checking problem for Lineal Time Logic (LTL) is studied in Chapter 10. Most of the contents of this chapter was published in [BKRS06]. We show that the LTL model checking problem is decidable for wPRS if we consider properties defined by formulae only with the strict eventually and strict always modalities. In the following section, we show that the model checking problem is decidable even for wPRS and LTL fragment based on modalities strict eventually, strict always, eventually in the strict past and always in the strict past. We establish the exact decidability border of model checking of wPRS classes and all basic modality fragments of LTL by showing that the model checking problems for PA and LTL(U), and for oo PA and LTL( F, X), are undecidable. Chapter 11 is devoted to model checking problems for LTL and extended process rewrite systems. LTLdet (introduced in [MaiOO]) is a common fragment of CTL and LTL. Using some results of the previous chapter we show that the model checking problem for wPRS and LTLdet is decidable. Our results of this chapter have not been published yet. 1.3 AUTHOR'S PUBLICATIONS 5 1.3 Author's Publications • Publications related to this PhD thesis - Journal papers [1] M. Křetínský, V. Řehák, and J. Strejček. Decidability of Reachability in Extended Process Rewrite Systems. Information and Computation, 2005. Submitted for publication. [2] M. Křetínský, V. Řehák, and J. Strejček. Refining the Unde-cidability Border of Weak Bisimilarity. In Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05), volume 149 of Electronic Notes in Theoretical Computer Science, pages 17-36. Elsevier Science Publishers, 2006. [3] M. Křetínský, V. Řehák, and J. Strejček. On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. In Philippe Schnoebelen, editor, Proceedings of INFINITY 2003, the 5th International Workshop on Verification of Infinite-State Systems, a satellite workshop of CONCUR 2003, volume 98 of Electronic Notes in Theoretical Computer Science, pages 75-88. Elsevier Science Publishers, 2004. - Conference and workshop papers [4] L. Bozzelli, M. Křetínský, V. Řehák, and J. Strejček. On Decidability of LTL Model Checking for Process Rewrite Systems. In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, volume 4337 of Lecture Notes in Computer Science, pages 248-259. Springer-Verlag, 2006. [5] V. Řehák. Weakly Extended Process Rewrite Systems. In MOVEP'06: 7th school on Modeling and VErifying parallel Processes, pages 360-364. Universitě de Bordeaux, 2006. Student's paper. [6] M. Křetínský, V. Řehák, and J. Strejček. Reachability of Hennessy-Milner Properties for Weakly Extended PRS. In R. Ramanujam and Sandeep Sen, editors, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, volume 3821 of Lecture Notes in Computer Science, pages 213-224. Springer-Verlag, 2005. [7] M. Křetínský, V. Řehák, and J. Strejček. Refining the Un-decidability Border of Weak Bisimilarity. In Preliminary Proceedings of the 7th International Workshop on Verification of 6 INTRODUCTION Infinite-State Systems (INFINITY'05), NS-05-4, BRICS Notes Series, pages 3-14. BRICS, 2005. [8] V. Řehák. Reachability for Extended Process Rewrite Systems. In MOVEP'04: 6th school on Modeling and VErifying parallel Processes, pages 77-82. Universitě Libre de Bruxelles, 2004. Student's paper. [9] M. Křetínský, V. Řehák, and J. Strejček. Extended Process Rewrite Systems: Expressiveness and Reachability. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory: 15th International Conference, volume 3170 of Lecture Notes in Computer Science, pages 355-370. Springer-Verlag, 2004. [10] M. Křetínský, V. Řehák, and J. Strejček. On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. In Preliminary Proceedings of the 5th International Workshop on Verification of Infinite-State Systems INFINTIY'2003, pages 73-85. Les Universités ä Marseille, 2003. - Technical reports [11] L. Bozzelli, M. Křetínský, V. Řehák, and J. Strejček. On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems. Technical Report FIMU-RS-2006-05, 27pp, Faculty of Informatics, Masaryk University, Brno, 2006. Full version of FSTTCS 2006 paper. [12] M. Křetínský, V. Řehák, and J. Strejček. Refining the Un-decidability Border of Weak Bisimilarity Technical Report FIMU-RS-2005-06, 20pp, Faculty of Informatics, Masaryk University, Brno, 2005. Full version of INFINITY 2005 paper. [13] M. Křetínský, V. Řehák, and J. Strejček. On the expressive power of extended process rewrite systems. Technical Report RS-04-07, 12pp, Basic Research in Computer Science, Aarhus, Denmark, 2004. [14] M. Křetínský, V. Řehák, and J. Strejček. Process Rewrite Systems with Weak Finite-State Unit. Technical Report FIMU-RS-2003-05, 23pp, Faculty of Informatics, Masaryk University, Brno, 2003. Full version of INFINITY 2003 paper. • Publications related to Liberouter project 1.3 AUTHOR'S PUBLICATIONS 7 - Conference and workshop papers [15] D. Antoš and V. Řehák. Routing, L2 Addressing, and Packet Filtering in a Hardware Engine. In Proceedings of the 2nd Doctoral Wokrshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), Mikulov, pages 1-8. FIT BUT, 2006. [16] P. Hlávka, V. Řehák, A. Smrčka, P. Šimeček, D. Šafránek, T. Vojnar. Formal Verification of the CRC Algorithm Properties. In Proceedings of the 2nd Doctoral Wokrshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), Mikulov, pages 55-62. FIT BUT, 2006. [17] A. Smrčka, V. Řehák, T. Vojnar, D. Šafránek, P. Matoušek, and Z. Řehák. Verifying VHDL Designs with Multiple Clocks in SMV. In 11th International Workshop on Formal Methods for Industrial Critical Systems FMICS 2006, 2007. To appear in LNCS series. [18] D. Antoš and V Řehák. Routing and Level 2 Addressing in a Hardware Accelerator for Network Applications. In ICT 2006,13th International Conference on Telecommunications. Funchal, Portugal, pages 1-4. Universidade da Madeira, 2006. [19] D. Antoš, V Řehák, and P. Holub. Packet Filtering for FPGA-Based Routing Accelerator. In CESNET Conference 2006, pages 161-173. CESNET, 2006. [20] T. Kratochvíla, V Řehák, and D. Šafránek. Formal Verification of a FIFO Component in Design of Network Monitoring Hardware. In CESNET Conference 2006, pages 151-160. CESNET, 2006. [21] D. Antoš, V Řehák, and J. Kořenek. Hardware Router's Lookup Machine and its Formal Verification. In 3rd International Conference on Networking ICN'2004 Conference Proceedings. Gosier, Guadeloupe, French Caribbean, pages 1002-1007. University of Haute Alsace, Colmar, France, 2004. [22] D. Antoš, J. Kořenek, and V Řehák. Lookups in IPv6 router implemented in an FPGA. In EurOpen, Proceedings of the 23rd conference, Strážnice, Czech Republic, pages 91-102, 2003. (in Czech). - Technical reports [23] P. Hlávka, T. Kratochvíla, V. Řehák, D. Šafránek, P. Šimeček, and T. Vojnar. CRC64 Algorithm Analysis and Verification. Technical Report 27, 7pp, CESNET, December 2005. 8 INTRODUCTION [24] J. Holeček, T. Kratochvíla, V. Řehák, D. Šafránek, and P Šimeček. Verification Process of Hardware Design in Liberouter Project. Technical Report 05, 7pp, CESNET, November 2004. [25] J. Holeček, T. Kratochvíla, V. Řehák, D. Šafránek, and P Šimeček. How to Formalize FPGA Hardware Design. Technical Report 04, llpp, CESNET, October 2004. [26] J. Holeček, T. Kratochvíla, V. Řehák, D. Šafránek, and P Šimeček. Verification Results in Liberouter Project. Technical Report 03,32pp, CESNET, September 2004. [27] T. Kratochvíla, V Řehák, and P. Šimeček. Verification of COMB06 VHDL Design. Technical Report 17, 17pp, CESNET, November 2003. [28] D. Antoš, J. Kořenek, K. Minaříková, and V. Řehák. Packet header matching in Comboó IPv6 router. Technical Report 01,15pp, CESNET, January 2003. [29] J. Barnat, T. Brázdil, P. Krčál, V Řehák, and D. Šafránek. Model Checking in IPv6 Hardware Router Design. Technical Report 07, 8pp, CESNET, July 2002. • Publication related to the author master thesis [30] V Řehák. ©-OBDD in Symbolic Model Checking. In M. Bielikova, editor, Proceedings of SOFSEM'02 Student Research Forum, pages 41-46, 2002. Chapter 2 Process Rewrite Systems (PRS) In this chapter we recall a definition of Process Rewrite Systems (PRS). PRS were introduced in [May97b] and a compact summary of the topic is nicely presented in [May98]. In Section 2.1 we introduce some basic notions behind are needed to define PRS in Section 2.2. In the next section we compare an expressive power of the defined PRS formalisms with respect to the strong bisimulation equivalence. 2.1 Basic Definitions Labelled Transition System We use a common notion of Labelled Transition System (LTS) for semantic definitions of infinite state systems. LTS is a well known formalism defined as follows. Definition 2.1. A labelled transition system (LTS) L is defined as a tuple (S, Act, —►, cko), where • S is a set of states or processes, • Act is a set of atomic actions or labels, • —> C (S x Act x S) is a transition relation, • cxo e S is a distinguished initial state. We write a —> ß instead of (a,a,ß) e—k A state ex e S is terminal (or deadlocked, written a —/-+) if there is no a e Act and ß e S such that a —> ß. The transition relation —► can be in a homomorphic way extended to finite sequences of actions a G Act* so as to write a —>* a and a —>* ß whenever a —> 7 —>* ß for some state 7. A state ß is reachable from a state a, written a —>* ß, if there is a G Act* such that a -—>■* ß. We say that a state is reachable if it is reachable from the initial state. 10 PROCESS REWRITE SYSTEMS (PRS) Equivalences on LTS In this thesis we define some classes of infinite state systems and naturally we would like to compare their expressive power. For the sake of the comparison an equivalence on the systems has to be chosen. We take into account isomorphism, strong bisimulation, and trace equivalence (also known as language equivalence). An isomorphism is the strongest relation of those mentioned above. Definition 2.2. A binary relation R on set of states S is an isomorphism if and only if it is a bijection and for each (a, ß) G R the following conditions hold: • Va' eS,aeAct:a^a' implies (3ß' G S : ß -^ ß' A (a', ß') G R) • V/3' G S, a G Act : ß -% ß' implies (3a' e S : a ^ a' A (a1, ß1) G R) If an isomorphism can be constructed between the initial states of two labelled transition systems then we say those labelled transition systems are isomorphic. The strong bisimulation is the second strongest relation of those we consider here. In context of studying process behaviour we are not interested in whether the relation between the systems is a bijection or not. Therefore the strong bisimulation does not have to be a bijection. Definition 2.3. A binary relation R on set of states S is a (strong) bisimulation [MU89] if and only if for each (a, ß) G R the following conditions hold: • Va'e5,oe4ci:aA«' implies (3ß' eS:/?A/3'A (a', ß1) G R) • V/3' G S, a G Act : ß -^ ß' implies (3a1 e S :a^a' A (a', ß1) G R) (Strong) bisimulation equivalence on an assumed LTS is the maximal bisimulation (i.e. union of all bisimulations). If a bisimulation can be constructed between the initial states of two labelled transition systems then we say those labelled transition systems are (strongly) bisimilar. In the case of trace equivalence we abstract away from the branching structure of a system and compare all possible executions only. Definition 2.4. A binary relation R on set of states S is a trace equivalence if and only if for each (a, ß) G R the following conditions hold: • y a' G S, w G Act* :a^U* a' implies (3ß' G S : ß ^* ß') • V/3' G S, w G Act* :ß^U*ß' implies (3a' G S : a -^U* a') If a trace equivalence can be constructed between the initial states of two labelled transition systems then we say those labelled transition systems are trace equivalent. As we work with systems describing processes in the thesis, we put the emphasise on strong bisimulation equivalence. We refer to [vG93] for more equivalences on processes. 2.1 BASIC DEFINITIONS 11 Process Terms The concept of Process Rewrite Systems (PRS) formalism is based on rewriting of process terms. Therefore, being able to define PRS, we have to define process terms at fist. Definition 2.5. Let Const = {X,...} be a countably infinite set of process constants. The set T of process terms (ranged over by t,...) is defined by the abstract syntax t::=e\X\ti.t2 \h\\t2, where • e is the empty term, • X g Const is a process constant (used as an atomic process), • 'W mean a parallel composition, and • '.' mean a sequential composition. We always work with equivalence classes of terms modulo commutativity and associativity of'W'and modulo associativity of'.' We also define e.t = t = t.e and t\\e = t. For every process term t, we define a set Const (t) to be the set of all constants occurring in the process term t. For the sake of the following definition we define four classes of process terms depending on whether the parallel composition and/or the sequential composition has been used in it. Definition 2.6. We distinguish four classes of process terms as: "1" terms consisting of a single process constant only (i.e. e £2) G R instead of (t\,a, £2) G R- Let A be a PRS as defined in Definition 2.7. We define Const(A) as the set of all constants occurring in the rewrite rules of A or in its initial state, and ^4c£(A) as the set of all actions occurring in the rewrite rules of A. We sometimes write (£1 °-> £2) G A instead of (£1 °-> £2) G R. Definition 2.8. The semantics of A is given by the LIS (S, Act(A), —>A,to), where • the set of states S = {£ G ß \ Const(ť) c Const(A)}, • the initial state of US £0 is formed by the initial term of A, and • the transition relation —>a is the least relation satisfying the following inference rules for all t\, £2, £ G S and a G ^4c£(A). (£l ■-> £2) G A £1 ^A £2 £l ^A £2 £1—>a £2 £i||£—>a£2||£ £i-£—>a £2-£ Note that parallel composition is commutative and, thus, the inference rule for parallel composition also holds with t\ and t exchanged. If no confusion arises, we sometimes speak about a "process rewrite system" meaning the "labelled transition system generated by a process rewrite system". We use —a. or —>r to emphasise that we mean the transition relation generated by a set of rules R and we also write —> instead of —a. if A is clear from the context. Remark 2.9. As there are only finitely many terms U and atomic actions cm such that £0 -^a U, it can be assumed without loss of generality that the initial state to of an (a, ß)-PRS is a single constant, say X0. 2.2 DEFINITION OF PROCESS REWRITE SYSTEMS 13 Every pair a, ß e {1,S,P,G} induces a class of all labelled transition systems that can be expressed by an (a, /3)-PRS. Some of the classes correspond to LTS classes of widely known models. In what follows we quote an apt descriptions of PRS classes as it was published in [Str02]: • (1,1)-PRS are equivalent to finite-state systems (FS). Every process constant corresponds to a state and the state space is bounded by | Const (A)\. Every finite-state system can be encoded as a (1,1)-PRS. • (1,5)-PRS are equivalent to Basic Process Algebra processes (BPA) defined in [BK85], which are the transition systems associated with Greibach normal form (GNF) context-free grammars in which only left-most derivations are allowed. • (1,P)-PRS are equivalent to communication-free nets, the subclass of Petri nets where every transition has exactly one place in its preset [BE97]. This class of Petri nets is equivalent to Basic Parallel Processes (BPP) [CHM93]. • (1, G)-PRS are equivalent to PA-processes, Process Algebras with sequential and parallel composition, but no communication (see [BK85] for details). • It is easy to see that pushdown automata can be encoded as a subclass of (S, S*)-PRS (with at most two constants on the left-hand side of rules). Caucal [Cau92] showed that any unrestricted (S, S*)-PRS can be presented as a pushdown automaton (PDA), in the sense that the transition systems are isomorphic up to the labelling of states. Thus (S, S*)-PRS are equivalent to pushdown processes (which are the processes described by pushdown automata). • (P, P)-PRS are equivalent to Petri nets (PN). Every constant corresponds to a place in the net and the number of occurrences of a constant in a term corresponds to the number of tokens in this place. This is because we work with classes of terms modulo commutativity of parallel composition. Every rule in A corresponds to a transition in the net. • (S, G)-PRS is the smallest common generalisation of pushdown processes and PA-processes. They are called PAD (PA + PDA) in [May97b]. (P, G)-PRS are called PAN-processes in [May97a]. It is the smallest common generalisation of Petri nets and PA-processes and it strictly subsumes both of them (e.g. PAN can describe all Chomsky-2 languages while Petri nets cannot). 14 PROCESS REWRITE SYSTEMS (PRS) • The most general case is (G, G)-PRS (here simply called PRS). PRS have been introduced in [May97b]. They subsume all of the previously mentioned classes. For some other intuition into the topic of PRS we refer to a very comprehensible introduction published by Esparza [Esp02] or Mayr's thesis [May98]. 2.3 Hierarchy of Process Rewrite Systems Figure 2.1 describes a hierarchy of (a, /3)-PRS classes with respect to strong bisimulation equivalence (bisimilarity). We call this hierarchy the PRS-hierarchy. More precisely, the classes of PRS systems are interpreted as the sets of their underlying labelled transition systems. The depicted hierarchy is then the upward oriented Hasse diagram of a partial order relation 'C' between these sets of labelled transition systems modulo bisimulation equivalence. In other words, a line connecting X and Y with Y placed higher than X means that every transition systems definable in X can be (up to bisimulation equivalence) defined in Y while the reverse does not hold - we write X C Y. Moreover, the classes that are not connected by any sequence of upward going lines are incomparable. The strictness of the hierarchy with respect to strong bisimulation equivalence follows from the results presented (or cited) in [BCS96, Mol96, MayOO], where the following systems are presented: • a BPP system which is not bisimilar to any PDA system, • a PN system which is not bisimilar to any PAD system, • a BPA system which is not bisimilar to any PN system, and • a PDA system which is not bisimilar to any PAN system. These systems imply strictness of all relations of the PRS-hierarchy Moreover, they also show incomparability of all non-related classes of the PRS-hierarchy. In what follows we exemplify the four aforementioned systems. To make references to these systems human readable, we assign intuitive acronyms to the systems; e.g. the system of Example 2.10 is called BPP non-PDA as it represents a BPP system which is not bisimilar to any PDA system. Example 2.10. (BPP non-PDA) A BPP system with the initial state X that is not bisimilar to any PDA system (for the proof see [Mol96]). 2.3 HIERARCHY OF PROCESS REWRITE SYSTEMS 15 PRS (G, G)-PRS PAD {S, G)-PRS PAN (P, G)-PRS PDA {S, S)-FRS PA (1,G)-PRS PN (P, P)-PRS BPA (l.SJ-PRS BPP (1,P)-PRS FS (1,1)-PRS Figure 2.1: The PRS-hierarchy 16 PROCESS REWRITE SYSTEMS (PRS) X^X\\B X^X\\D Im£ B^e D^e It follows from Example 2.10 that classes BPP, PA, and PAD are not contained ($Z) in any of classes FS, BPA, and PDA. We write BPP, PA, PAD £ FS, BPA, PDA. Example 2.11. (PN non-PAD) A Petri net given as (P, P)-PRS with the initial state X || A\\B that is not bisimilar to any PAD process (for the proof see [MayOO]). X^XWAWB YWA^Y XWA^Z Y\\aA Z i^y y\\b^y x\\B^z Y\\B^z Intuitively, the system models two counters running in parallel with a synchronised increasing (action g) and a synchronised switching to decreasing phase (action c) and deadlock state (action d). It follows from Example 2.11 that classes PN, PAN, and PRS are not contained ($Z) in any of classes BPP, PA, and PAD. We write PN, PAN, PRS £ BPP, PA, PAD. Example 2.12. (BPA non-PN) A BPA system with the initial state X that is not bisimilar to any PN system (for the proof see [Mol96]). X^X.A X^X.B Im£ A^e B^e It follows from Example 2.12 that classes BPA, PA, and PAN are not contained ($Z) in any of classes FS, BPP, and PN. We write BPA, PA, PAN £ FS, BPP, PN. Example 2.13. (PDA non-PAN) A PDA system with the initial state U.X that is not bisimilar to any PAN system (for the proof see [MayOO]). U.X A U.A.X U.A ^ U.A.A U.B A U.A.B U.X <\ U.B.X U.A ^ U.B.A U.B <\ U.B.B U.X A V.X U.A A V.A U.B A V.B U.X A W.X U.A A W.A U.B A W.B V.X ^V V.A^V V.B^V W.X A W W.A A W W.B A W Intuitively, the system behaves as a pushdown automaton with control states U, V, W and stack alphabet {X, A, B}. Symbol X marks the bottom of the stack and symbols A and B save sequential information. 2.3 HIERARCHY OF PROCESS REWRITE SYSTEMS_____________________17 It follows from Example 2.13 that classes PDA, PAD, and PRS are not contained (£) in any of classes BPA, PA, and PAN. We write PDA, PAD, PRS £ BPA, PA, PAN. Concerning the other equivalences, let us note that strictness of the PRS-hierarchy with respect to strong bisimulation implies strictness also with respect to isomorphism. Contrary to this, the PRS-hierarchy is not strict with respect to trace equivalence, e.g. both BPA and PDA define the class of e-free context-free languages. 18__________________________________PROCESS REWRITE SYSTEMS (PRS) Chapter 3 State Extended PRS (sePRS) Most research (with some recent exceptions, e.g. [BT03, Esp02]) has been devoted to the PRS classes from the lower part of the PRS-hierarchy depicted in Figure 2.1, especially to pushdown processes (PDA), Petri nets (PN) and their respective subclasses. Let us recall the successes of PDA in modelling recursive programs with value passing from callee to caller (without process creation), PN in modelling dynamic creation of communicating concurrent processes (without recursive calls), and communicating pushdown systems (CPDS) [BET03] as an example of modelling both features. All of these formalisms subsume a notion of a finite-state control unit keeping some kind of global information which is accessible to the redexes (the components that can be reduced) of a PRS term - hence a finite-state control unit (FSU) can regulate rewriting. 3.1 Definition of State Extended PRS In this section, we introduce an extension of process rewrite system formalism that enriches every PRS system with an FSU, as given in [JKM01]. We call these systems state extended PRS and define them as follows. Definition 3.1. Let Act = {a,b,- ■ ■} be a countably infinite set of atomic actions and a, ß G {1, S, P, G} such that a c ß. An (a, /3)-sePRS A is a tuple (M, R, mo, to), where • M is afinite set of states of a control unit, • líc ((M x (a\ {e})) x Act x (M x ß)) is afinite set of rewrite rules, • mo G M is an initial state of the control unit, and • to G ß is an initial term. We write ((m,ti) ^-> (n,Í2)) G Rinsteadof((m,ti),a,(n,t2)) G R. 20 STATE EXTENDED PRS (sePRS) To shorten our notation we write mt instead of (m, t). As in the PRS case, instead of {mt\ c-^ nt2) G R where A = (M,R,mo,to), we usually write (mil °-*- ^2) S A. The meaning of Const(A) (process constants used in rewrite rules or in to) and Act (A) (actions occurring in rewrite rules) for a given state extended PRS A is also the same as in the PRS case. Moreover, we use M (A) to denote the finite set of control states which occur in A. Definition 3.2. The semantics of a state extended (a, ß)-PRS system A is given by the corresponding labelled transition system (S, Act(A), —a, moto), where • S = M (A) x{teß\ Constat) C Const(A)}, • moto is the initial state composed of the initial control state mo of the control unit M (A) and the initial term to, and • the transition relation —a is defined as the least relation satisfying the following inference rules for all mt\, nČ2, rn{ti\\t), m(Í2p), n(t\.t), nfo-t) G S and a e Act (A). (mil °-*- nt2) e A mil —-»a ^2 rnti —>a ^2 mti -%\ nt2 m(ti\\t) -%\ «top) m(íi.í) -%\ n(Č2-č) Note that parallel composition is commutative and, thus, the inference rule for parallel composition also holds with t\ and t exchanged. Instead of (1, l)-sePRS, (1, S)-sePRS, (1, P)-sePRS, (S, S)-sePRS, (1, G)-sePRS, (P, P)-sePRS, (S, G)-sePRS, (P, G)-sePRS, and (G, G)-sePRS we use a more natural notation seFS, seBPA, seBPP, sePDA, sePA, sePN, sePAD, sePAN, and sePRS respectively. The class seBPP is also known as multiset automata (MSA) or parallel pushdown automata (PPDA), see [Mol96]. 3.2 Hierarchy of State Extended PRS In this section we present an overview of expressive power of the defined classes. Figure 3.1 shows a graphical description of the PRS-hierarchy enriched by the state extended (a, /3)-PRS classes. We call the hierarchy the state extended PRS-hierarchy. The dotted lines represent the relations where the strictness is only our conjecture. An immediate observation is that the classes FS, PDA, and PN have exactly (i.e. up to isomorphism) the same expressive power as the corresponding state extended classes. We note some other trivial observations also even up to isomorphism: X c Y implies seX c seY for every two classes X and Y of PRS 3.2 HIERARCHY OF STATE EXTENDED PRS 21 sePRS sePAD PRS sePAN PAD sePA PAN sePDA=PDA=seBPA PA BPA sePN=PN seBPP=PPDA BPP seFS=FS Figure 3.1: The state extended PRS-hierarchy 22 STATE EXTENDED PRS (sePRS) (a, /3)-PRS C (a, /3)-sePRS for all (a, /3)-PRS. Looking at two lines leaving sePA down to the left and down to the right, we note the "left-part collapse" of (S, 5)-PRS and PDA proved by Caucal [Cau92] (up to isomorphism). The right-part counterpart is slightly different due to Moller's result establishing PPDA c PN [Mol98]. Therefore, the previous trivial observations imply only PPDA C sePA and the relation between PN and sePA left open. In Subsection 3.2.1 we prove that PN c sePA. In Subsection 3.2.2 we discuss strictness ('c') of the state extended PRS-hierarchy. 3.2.1 PN C sePA Here we show that Petri nets are less expressive (with respect to the strong bisimulation equivalence) than state-extended PA processes. Let A be a Petri net and Const(A) be a set of k process constants {X\,... ,Xk}. Speaking about PN systems in context of PRS, Xn denotes a parallel composition of n copies of X. In this subsection we consider Petri nets in the traditional "place-transition" setting where "markings" are the counterparts of the states of LTSs, see e.g. [Pet81, Rei85]. Let the Petri net A have k places Pi,..., Pk, each state yPi\\ \wPk xx || ■■■\\xk of the PN A is called marking and it is written as (Pi,---,Pk) where Pi is the number of tokens at the place Pi. Any rewrite rule vh\\ n vh J\ yriii m vrk Ai \\---\\Xk ^ Xx ||...||Afc (where h,r% > 0) is called transition and it is written as (h,...,lk) ^ (ri,...,rk). As we employ the marking-place description of PN, Xn stands only for a sequential composition of n copies of X in the rest of the subsection . The heart of our argument is a construction of an sePA A' that is bisimi-lar to the given PN A. The main difficulty in this construction is to maintain the number of tokens at the places of a PN. To this end, we may use two types of sePA memory: • a finite control (FSU), which cannot represent an unbounded counter, • a term of an unbounded length, where just one constant can be rewritten in one step. 3.2 HIERARCHY OF STATE EXTENDED PRS 23 Intuition Our construction of an sePA A' can be reformulated on intuitive level as follows. Let a marking (pi,...,Pk) mean' that we have Pi units of the i-th currency, i = 1,..., k. An application of a PN transition (h,...,lk) ^ (ri,...,rk) has an effect of a currency exchange from pi to Pi — h + r i for all i. An sePA reseller A' will have k finite pockets (in its FSU) and k bank accounts (a parallel composition of k sequential terms U). The reseller A' maintains an invariant pi = pocketi + accounti for all i. To mimic a PN transition he must obey sePA rules, i.e. he may use all his pockets, but just one of his accounts in one exchange — transition. A solution is to do pocketi <->■ accounti transfers cyclically, i = 1,..., k. Hence, rebalancing pocketi the reseller A' must be able to perform the next k — 1 exchanges (while visiting the other accounts) without accessing accounti. Therefore, A' needs sufficiently large (but finite) pockets and sufficiently high (and still fixed) limits for pocketi <->■ accounti transfers. In what follows we show that these bounds exist. Bounds In one step the amount of the i-th currency can be changed at most by Li = max {k,n \ (h,..., Ik) °-> (n, • • •, rk) is a PN transition}, thus the upper bound for the total effect of k consecutive steps can be set up to Mi = k- Li. Any rebalancing of the i-th pocket sets its value into {Mi,...,2Mi-l} (or into {0,..., 2Mi — 1} if accounti is empty). Hence, after k transitions the value of pocketi is in {0,...,3Mi-l}. Then the next rebalancing takes place and accounti is increased or decreased (if it is not empty) by Mi to achieve the (rebalanced) value of pocketi in {Mi,...,2Mi-I}. Construction Each state of sePA A' consists of a state of an FSU and a term (parallel composition of k stacks, in fact just counters, representing accounts). Each state of the FSU is a member of the following product. 24 STATE EXTENDED PRS (sePRS) {!,..., k} x {0,...,3Mi-l} x ... x {0,...,3Mfc-l} update controller pocketi pocketk The update controller goes in round-robin fashion on its range and refers to the account being updated (rebalanced) in the next step. The value of each pocketi (subsequently denoted by rrii) is equal to the number of tokens at Pi counted modulo Mj. We define 2k process constants Bi, Xi e Const(A'), where i = 1,..., k. The í-th stack U is of the form Xf.Bt where n> 0, Bi represents the bottom of the i-th stack, and each Xi represents Mi tokens at place Pi. Given an initial marking ao = {p\,..., Pk) of A, we construct the initial state ßo = (l,mi,...,mfc)či|| ••• ||ífc of the sePA A', where denoting rii = max(0, (pi div Mi) — 1) we put rrii = Pi — rii ■ Mi and U = X"\Bi. In other words we have Pi = rrii + rii ■ Mi and moreover rrii e {Mi,..., 2Mi — 1} if pi is big enough (i.e. pi > Mi). To each transition (l\,... ,lk) °-*- (^i, • • •, fk) of PN A we construct the set of sePA rules (s, mi, ■ ■ ■, rrik) t A {s1, m\,..., m'k) ť such that they obey the following conditions: • Update controller conditions: - s,s' G {1,... ,k} and - s' = (s mod k) + 1. • General conditions for pockets (1 < i < k): ml,mie{0,...,3Ml-l}/ - rrii > k (i-e. the transition "is enabled"), and - if i / s then m'i = rrii — h + f i. • The case i = s means to specify m's and the terms t, ť that acts the pocket-account rebalancing transaction. These are given by the rules of the following table. The first two Bottom rules are the rules for working with the empty stack. The next three Top rules describe the rewriting of process constant Xs. Depending on the value of Wl = rns — ls + rs, there are dec, inc, and basic variants manipulating the s-th stack. 3.2 HIERARCHY OF STATE EXTENDED PRS 25 Rule t ms G ms ť Bottom-basic rule Bs R.. .,2MS-1} m; Bs Bottom-inc rule Bs {2MS, ..,3MS-1} Ws~ — Ms Xg.Bg Top-dec rule Xs {o,. •, Ms - 1} wrs + Ms £ Top-basic rule Xs {Ms,. ..,2MS-1} m; Xs Top-inc rule Xs {2MS, ..,3MS-1} Ws~ — Ms Xg-Xg Theorem 3.3. PN c sePA with respect to bisimulation equivalence. Proof. Let A be an arbitrary PN with an initial marking ao. According to the construction given above we build the sePA A' with the initial state ßo. In the rest of the proof we show that a relation R = {(a, ß) | marking a is (pi,... ,pk) Aß = (s,m1,...,mk)X^.B1\\...\\X^.Bk A S G {1, ...,k} A for alii = 1,... ,k it holds that Pi = rrii + rii ■ Mi A rrii < 2Mi + (s — i mod k)Li A if rii > 0 then Mi — (s — i mod k)Li < rrii else 0 < rrii} is a bisimulation between A and A'. It follows directly from the construction that the pair (cto,ßo) of the initial states is in R. We follow the definition of bisimulation to prove that the relation R is a bisimulation. Let a = (pi,..., pk) be a marking of PN A and ß = {s,ml,...,mk)X^.Bl\\...\\Xlk.Bk be a state of sePA A' such that (a, ß) G R. Let us assume that a transition (l\,..., lk) c-^ (ri,..., rk) is fired in a and leads to a' = (p[,... ,p'k), i.e. Pi > k and p^ = Pi — k + r i, for all i = 1,..., k. According to the definition of bisimulation, we will show that there is also a state ß1 of A' and a transition with a label a leading from ß to ß' such that (a', ß') G R. Looking into the construction it is easy to see that such transition exists if rrii > k for alH = 1,..., k. These inequalities can be easily proved as follows. For each i = 1,..., k, we discus two cases: • If rii = 0 then (a, ß) G R implies Pi = rrii+rii-Mi = rrii. This, together with pi > U, directly leads to the desired rrii> k. • If rii > 0 then (a, ß) G R implies Mi —{s —i mod k)Li < rrii. As Mi is defined to be equal tok ■ Li, we get that rrii > Li. Now, the definition of Li implies Li > k that directly results in rrii> k. 26 STATE EXTENDED PRS (sePRS) It remains to show that (a', ß') e R. This can be obtained by a straightforward inspection through the definitions of all the rule types. The symmetric case, starting with a transition from ß, proceeds in a similar way. Hence, A and A' are bisimilar and so PN C sePA in our notation. D We note that the sePA system constructed by our algorithm does not need to be isomorphic to the original PN system, e.g. due to the different values of the update controller. 3.2.2 Strictness and Incomparability To show the strictness ('C') of all relations of the state extended PRS-hierarchy and incomparability of all non-related classes of the state extended PRS-hierarchy the following examples have to be presented: • a BPP system which is not bisimilar to any PDA system, • a PPDA system which is not bisimilar to any PAD system, a PN system which is not bisimilar to any PPDA system, • a PAN system which is not bisimilar to any sePAD system, • a BPA system which is not bisimilar to any PN system, • a PDA system which is not bisimilar to any PAN system, • a PAD system which is not bisimilar to any sePAN system, and • an sePA system which is not bisimilar to any PRS system. For the non-bold items we simply refer to Section 2.3, where the systems are exemplified. Concerning the first bold item we focus on the PN non-PAD system of Example 2.11. In terms of traditional Petri net notation, we can say that the places X, Y, and Z are 1-bounded1 and the places A and B are unbounded.2 As there is no communication3 between the unbounded places A and B, it is well known that the PN system can be redefined as a PPDA system. Using this we have constructed the PPDA of Example 3.4. It is easy to see that the PPDA system of Example 3.4 is isomorphic to the PN system of Example 2.11. *A place is 1-bounded if it contains at most one token in each reachable marking. 2 A place is unbounded if there is no bound on the number of tokens. 3Two places communicate, if they are input places of the same transition. 3.2 HIERARCHY OF STATE EXTENDED PRS 27 Example 3.4. (PPDA non-PAD) A PPDA given as (1, P)-sePRS with the initial state xC\\A\\B that is not bisimilar to any PAD process (it follows from Example 2.11). xCc-^ xC\\A\\B yA^ye xA^ze yAc^ ze xC^yC yB^ye xB A ze yB A ze It follows from Example 3.4 that classes PPDA, sePA, and sePAD are not contained (£) in any of classes BPP, PA, and PAD. We write PPDA, sePA, sePAD % BPP, PA, PAD. The system of the second item written in bold (PN non-PPDA system) was conjectured in [Mol96] and proved in [Mol98] later on. The PN system of this papers is presented in the following example. Example 3.5. (PN non-PPDA) A PN given as (P, P)-PRS with the initial state X that is not bisimilar to any PPDA process (for the proof see [Mol98]). X^X\\A X\\A\\B^X Y\\A^Y X^X\\B X^Y Y\\A^Y It follows from Example 3.5 that PN £ PPDA. Concerning language equivalence, we mention that the PN languages can be fully characterised in terms of PPDA. This result on language equivalence between PN and PPDA classes has not been published but only presented by Hirshfeld in his talk "Methods and tools for the verification of infinite state systems" in Grenoble, March 97 [Hir]. To finish the strictness and incomparability proofs of the state extended PRS-hierarchy (with respect to strong bisimulation equivalence), it remains to show a PAD non-sePAN system, a PAN non-sePAD system, and an sePA non-PRS system. Unfortunately, according to our best knowledge, the existence of these systems have not been proved yet. Therefore, five lines remain dotted in the state extended PRS-hierarchy. In the following, we give an intuition that supports our conjecture that all the relations are strict. Intuition and Conjectures Let us provide some intuition to qualify differences between the classes of of the state extended PRS-hierarchy. First, let us discus modelling abilities implied by terms forming right-hand sides of PRS rules. A sequential composition on the right-hand side 28 STATE EXTENDED PRS (sePRS) allows us to model sequential execution of other processes; hence an arbitrary long sequential information can be stored. A parallel composition on the right-hand side of rules enables to store information as multisets. Composed terms (i.e. terms not belonging to 1 class) on the left-hand sides of rules upgrade the formalism from "context-free" level onto "context-sensitive" one. This lifting serves to model communication between modelled processes; in particular, the process behaviour is sensitive to its sequential and/or parallel context. The sequential "context-sensitivity" can solve a problem how to sent a return value to the parent process (e.g. X.P —> P" instead of X —> e). The parallel operator on the left-hand side of rules can serve for synchronisation (and value passing) between parallel siblings. For example BPP=(1, P)-PRS systems, also called "communication free Petri nets," represent a context-free formalism whereas PN=(P, P)-PRS systems form its context-sensitive counterpart. Extensions with a control finite-state unit (FSU) bring further possibilities to increase expressive power of a system. On the one hand, such extensions are similar to the left-hand side extensions because it brings communication between different subterms, but on the other hand an FSU controls the whole of rewritten term and so we suggest that it cannot completely supply the local communication. The global communication abilities coincide with the local ones in the case of BPA only, where all communicating process terms are in one location and so (1, S')-sePRS=seBPA=PDA=(S', S)-PRS. We conjecture that in more powerful classes (such as PA, PAD, PAN, PRS) there are state-extensions orthogonal to the PRS-hierarchy In the following example we present systems that supports our conjecture. Example 3.6. (PAD non-sePAN) A PAD system with the initial state Y that is not bisimilar to any sePAN (according to our conjecture). Y^(U.X)\\Y U.X A U.A.X U.A ^ U.A.A U.B A U.A.B II.X <\ U.B.X U.A ^ U.B.A U.B <\ U.B.B U.X A V.X U.A A V.A U.B A V.B U.X A W.X U.A A W.A U.B A W.B V.X ^V V.A^V V.B^V W.X i W W.A A W W.B A W Intuitively, the system behaves as arbitrary many PDA non-PAN systems (Example 2.13) running in parallel. Each such a system needs to store an unbounded piece of sequential information, hence a sequential operator has to be employed. Moreover, the PAD non-sePAN system consists of an unbounded number of such systems running in parallel. As the term part is the only unbounded part of every state ofsePAN system, zve suppose that the term part of a desired sePAN has to be 3.2 HIERARCHY OF STATE EXTENDED PRS 29 organised in a similar way as in the case of the examined PAD, i.e. an unbounded number of unbounded sequential terms connected by parallel operators. In what follows we want to indicate that an FSU extension cannot fully supply the communication over a sequential operator in this case. The most significant "communication over a sequential operator" is to carry some information during decreasing of the sequential stack, i.e. changing the process constants "bellow" a sequential operator during erasing the "topmost" process constant. In an sePAN system, every rewrite rule rewrites only parallel subterms, hence, such a caring of information has to be divided into more then one step. The problem is that there is an unbounded number of stacks, and so in a subsequent step we cannot remember which stack was decreased in the previous step. Contrary to the technique used in the proof showing PN^sePA (see Subsection 3.2.1), where the number of stacks is bounded, the stacks of the speculated sePAN cannot be distinguished using different process constants. Moreover, in the PN^sePA construction, FSU stores a reference to the stack rebalanced in the last step. Here, the reference can be arbitrary large and so it does not fit into any FSU. Example 3.7. (PAN non-sePAD) A PAN system with the initial state Y that is not bisimilar to any sePAD (according to our conjecture). Y^((X\\A\\B).U)\\Y X^X\\A\\B Y\\A^Y X\\A^Z Y\\A^ Z lAľ ľ|BÍľ X\\B^Z Y\\B^Z The system behaves as arbitrary many PN non-PAD systems (Example 2.11) running in parallel. The term construction ".U" forms a communication barrier between the respective Petri net systems. Similarly to the previous case, we conjecture that unbounded number of unbounded Petri net implies that the term part of the system has to be constructed in the same way as in this example regardless of which state extended PRS formalism we use. Therefore, using the same argumentation as above, we conclude that the local synchronisation in the subsystems cannot be supplied be the global communication via an FSU. The last system is necessary for the incomparability result only. It implies, among others, that sePA ^ PRS. Example 3.8. (sePA non-PRS) An sePA system with the initial state qX\\Y that is not bisimilar to any PRS (according to our conjecture). qX ^ qX.A pY A pY.C oA ^ oe b y b' qX <—> qX.B pY ^ oe oB ^-> oe qY A qY.C oC ^ oe qX <—> pe 30 STATE EXTENDED PRS (sePRS) It is easy to see that the system is isomorphic to the system of Example 4.9. It was conjectured that there is no PRS bisimilar to the system. In [Str02] there is an intuitive argumentation that supports the conjecture (see Example 4.9 for further details). Chapter 4 PRS with Finite Constraint Systems (fcPRS) In this chapter we recall an extension of process rewrite systems with finite constraint systems (fcPRS). This extension has been introduced by Strejček in [Str02]. A motivation comes from the theory of constraint systems used in concurrent constraint programming (CCP) - see e.g. [SR90]. Contrary to the state extended PRS, fcPRS employs a restricted finite state unit. The unit behaves as a shared CCP store which is seen as a set of constraints on the values that common variables can represent. 4.1 Definition of PRS with Finite Constraint Systems In the following definition we define a constraint system as a set of constraints with a structure of an algebraic lattice. A constraint system describes a state space and possible evolution of a CCP store unit. Definition 4.1. A constraint system is a bounded lattice (C, \-, A, tt,ff), where • C is a set of constraints, • h (called entailment) is an ordering on this set, • A is the least upper bound operation, and • tt, ff (true and false) are the least and the greatest elements of C respectively (ffhttandtt^ff). In algebra, the symbol A usually denotes the greatest lower bound operation, while the least upper bound operation is rather marked with symbol V. Here we use a notation of CCP where the least upper bound corresponds to logical conjunction. 32 PRS WITH FINITE CONSTRAINT SYSTEMS (fcPRS) Example 4.2. Examples of constraint systems, ff o m n tt Using the notion of finite constraint systems we can define process rewrite systems with finite constraint system in the following definition. Definition 4.3. Let Act = {a,b,- ■ ■} be a countably infinite set of atomic actions and a,ß e {1,5*, P, G} such that a c ß. An (a,/3)-fcPRS (PRS with finite constraint system) is a tuple A = (C, R, tt, to), where • C = (C, h, A, ttjf) is a finite constraint system describing the store; the elements of C represent values of the store, • R c ((C x (a\ {e})) x Act x (C x /?)) is afinite set of rewrite rules, • tt is the least element ofC, and • to G ß is a distinguished initial process term. We write ((m,ti) ^-> (n, Č2)) s R instead of ((m, ti), a, (n, Í2)) e -R- To shorten our notation we write mt instead of (m,t). As in the PRS case, instead of {mt\ c-^ nt2) G R where A = (C, R, tt, to), we usually write (mil °-*- ^2) S A. The meaning of Const(A) (process constants used in rewrite rules or in to), Act(A) (actions occurring in rewrite rules), and M (A) (values of the store occurring in A) for a given fcPRS A is the same as in the sePRS case. 4.1 DEFINITION OF PRS WITH FINITE CONSTRAINT SYSTEMS 33 Definition 4.4. The semantics of an (a, ß)-fcPRS system A = (C,R,tt,to) is given by the ĽTS (S, Act(A), —a, tt to), where • S = (M (A) \ \ff\) x {t G ß I Constat) c Const(A)} is the set of states, • tt to is the initial state composed of the least element tt of the store M (A) and the initial term to, and • the transition relation —a is defined as the least relation satisfying the following inference rules for all mt i, ni2, ot\, (o An)i2, m(íi||í), m(i2||i), n(ti.t), n(t2-t) G S and a G Act (A). (míi ^ nt2) e A ----------------------- if oh mando An^ff ot\ —>a (o A n)í2 mil —>a ^Í2 míi —>a nt2 m(íi||í) -%\ n(t2\\t) m(h.t) -%\ n(t2-t) Note that parallel composition is commutative and, thus, the inference rule for parallel composition also holds with t\ and t exchanged. The two side conditions in the first inference rule are very close to principles used in CCP. The first one (o h m) ensures the rule (mti °-> ni2) G A can be used only if the current value of the store o entails m (it is similar to ask(m) in CCP). The second condition (o A n / ff) guarantees that the store stays consistent after application of the rule (analogous to the consistency requirement when processing tell(n) in CCP). An important observation is that the value of a store can move in a lattice only upwards as o A n always entails o, i.e. o A n is greater than or equal to o. Intuitively, partial information can only be added to the store, but never retracted. We say that the store is monotonie. Let o be a store value of an fcPRS state and (mil °-> ni2) G A be a rule that can be applied on the state. The fcPRS definition says that ohm and o An / ff where o An is the store value of the state reached by the application. It follows from the monotonicity of the store that, for every subsequent value p of the store, p \- m. Moreover, associativity, commutativity, and idempotence of the least upper bound operation A imply that p An = p for every subsequent store value p, and so every rule can change the store only during the first application. To sum up, we note that p\- m and p An / ff for every subsequent store value p, i.e. any further application of a rule cannot be forbidden by a value of the store. Instead of (l,l)-fcPRS, (1, S)-fcPRS, (l,P)-fcPRS, (S, S)-fcPRS, (1,G)-fcPRS, {P, P)-fcPRS, {S, G)-fcPRS, {P, GQ-fcPRS, and {G, G)-fcPRS we use a more natural notation fcFS, fcBPA, fcBPP, fcPDA, fcPA, fcPN, fcPAD, fc-PAN, and fcPRS respectively. 34 PRS WITH FINITE CONSTRAINT SYSTEMS (fcPRS) 4.2 Hierarchy of PRS with Finite Constraint Systems In this section we present an overview of expressive power of the defined classes. Figure 4.1 shows a graphical description of sePRS-hierarchy enriched by (a, /3)-fcPRS classes. The hierarchy is constructed with respect to strong bisimulation. The dotted lines represent the relations where the strictness is only conjectured. It is an easy observation that (a,/3)-PRS c (a,/3)-fcPRS c (a,/3)-sePRS holds for (a, /3)-PRS class (even up to isomorphism). Moreover, we note that for every two classes X and Y of PRS X c Y implies fcX c fcY. The strictness of the relations depicted in Figure 4.1 follows from the following examples: • a BPP system which is not bisimilar to any PDA system, • a fcBPP system which is not bisimilar to any PAD system, • a PPDA system which is not bisimilar to any fcPAD system, • a PN system which is not bisimilar to any PPDA system, • a PAN system which is not bisimilar to any sePAD system, • a BPA system which is not bisimilar to any PN system, • a fcBPA system which is not bisimilar to any PAN system, • a PDA system which is not bisimilar to any fcPAN system, • a PAD system which is not bisimilar to any sePAN system, • a fcPA system which is not bisimilar to any PRS system, and • a sePA system which is not bisimilar to any fcPRS system. For the bold items we simply refer to the previous sections where the systems are presented. In what follows the non-bold systems are exemplified. 4.2 HIERARCHY OF PRS WITH FINITE CONSTRAINT SYSTEMS 35 sePDA=fcPDA=PDA=seBPA seFS=fcFS=FS Figure 4.1: The fcPRS classes and the state extended PRS-hierarchy 36 PRS WITH FINITE CONSTRAINT SYSTEMS (fcPRS) Example 4.5. (f cBPP non-PAD) Let us consider a fcBPP system given as an (1, P)-fcPRS with the constraint system depicted below and the initial process term X. ff ttx A ttx\\A I ttX <\ ttX\\B 0 ttX A oe | oA A tte oB c-^ tte There is no PAD system bisimilar to the considered fcBPP system (for the proof see [Str02]). It follows from Example 4.5 that classes fcBPP, fcPA, and fcPAD are not contained (£) in any of classes BPP, PA, and PAD. We write fcBPP, fcPA, fcPAD £ BPP, PA, PAD. Example 4.6. (PPDA non-fcPAD) Let A be a PPDA process with the initial state xC\\A\\B and the following rewrite rules: xC^xC\\A\\B yA^ye A d xA c—> ze A d y A c—> ze xC^yC yB^ye xB "-^ ze yB "-^ ze yC^zC a e z A c—> ze zB c—> ze zC^xC\\A\\B The system A is the same as the PPDA non-wPAD of Example 5.10. Hence, there is nofcPAD system bisimilar to the considered PPDA A (the proof directly follows from Lemma 5.11). It follows from Example 4.6 that classes PPDA, sePA, and sePAD are not contained (£) in any of classes fcBPP, fcPA, and fcPAD. We write PPDA, sePA, sePAD % fcBPP, fcPA, fcPAD. Example 4.7. (fcBPA non-PAN) Let A be afcBPA of the form (C, R, tt, U.X), where C and R are as follows. ff ttU A ttU.A ttA A tte / \ ttU ^ ttU.B ttB <\ tte m n \ / tt C 6 ttU c—> me mX c—> tte b f ttU °-> ne nX ^-> tte The system A is not bisimilar to any BPA (for the proof see [Str02]). It follows from Example 4.7 that classes fcBPA, fcPA, and fcPAN are not contained ($Z) in any of classes BPA, PA, and PAN. We write fcBPA, fcPA, fcPAN £ BPA, PA, PAN. 4.2 HIERARCHY OF PRS WITH FINITE CONSTRAINT SYSTEMS 37 Example 4.8. (PDA non-fcPAN) A PDA system with the initial state U.X.Y that is not bisimilar to anyfcPAN (for the proof see [Str02]). U.X A U.A.X U.A A U.A.A U.B a U.A.B II.X <\ U.B.X U.A ^ U.B.A U.B b U.B.B II.X A V.X U.A A V.A U.B c V.B u.x A w.x U.A A W.A U.B d W.B v.x^v V.A^V V.B' b V w.x^w W.A^W W.B b >w V.Y A U.X.Y W.Y A U.X.Y V.Y^Z W.Y A Z It follows from Example 4.8 that classes PDA, sePA, and sePAN are not contained ($Z) in any of classes fcBPA, fcPA, and fcPAN. We write PDA, sePA, sePAN % fcBPA, fcPA, fcPAN. Intuition and Conjectures Similarly to the state extension of PRS, finite constraint systems bring some kind of global communication as well. But a constraint system is more restricted than a finite state unit. Let us recall monotonicity of the store and the feature stating that any further application of a rule cannot be forbidden by a value of the store. Therefore, we conjecture that (a,/3)-PRS c (a,/3)-fcPRS c (a,/3)-sePRS holds for each (a, /3)-PRS except for FS, PDA, and PN, where it is known that (a, ß)-PRS = (a, /3)-sePRS. Example 4.9. (f cPA non-PRS) Let Abe a fcPA system with the initial process term X\\Y and the following constraint system and rewrite rules. ff ttX ^ ttX.A oA ^ tte ttX A ttX.B oB ^ tte ttY A ttY\\C oC £* tte ttX A pe pY "-^ oe p I tt It was conjectured that there is no PRS bisimilar to this fcPA system A. In [Str02] there is the following intuitive argumentation that supports the conjecture. The behaviour of A defined in the example above is as follows. At the beginning, the process X can perform some actions a, b and remember the order of the 38 PRS WITH FINITE CONSTRAINT SYSTEMS (fcPRS) actions, while the process Y can perform just the action c and count the number of performed actions c. The process X can also perform the action x, make a remark p on the store about this action and terminate. Thereafter, the process Y can perform the action y, make a remark o on the store and terminate. When both processes X and Y are terminated (i.e. there is p A o = o on the store), actions a', b', d can be performed. The order (and the count) of actions a', b' corresponds in reversed order to actions a, b produced before termination of the process X. The count of actions d is the same as the count of actions c performed before termination of the process Y. We can approve that thisfcPA system is not bisimilar to any PAD process. For the proof we consider the fcPA process without rules labelled by the action b (if we assume that there is a PAD process bisimilar to the original fcPA, then there is also a PAD system without b action bisimilar to the fcPA without b action). Then the behaviour of our system is very similar to the behaviour of fcBPP from Example 4.5, which is not bisimilar to any PAD process. The proof is very similar too. We can also approve that the considered fcPA process is not bisimilar to any Petri net. The argumentation is based on the fact, that if we remove the rules labelled by c from thefcPA system, then we get a system describing the language L = {w.x.y.wR | w G {a, b}*}. The proof that there is no Petri net generating the language L, can be found in [Pet81]. Now we try to explain (on very intuitive level) why we think that there is no PRS process bisimilar to the considered fcPA. Let us assume that A is such a bisimilar PRS system. We know this PRS cannot be described by any PAD process. Thus, there must be reachable state with some parallel composition. As the use of the parallel composition must be "non-removable", the information about performed actions a, b, c should be stored in some components of this parallel composition. There should be one parallel component (let us call it p) which saves the information about the order of actions a, b (and thus p is a sequential composition, at least at the top-level), and another parallel component (let us call it q) which remembers the number of performed actions c (the information about the count of actions c cannot be mixed with the information about the order of actions a, b, because after the action y we need a "random access" to the count of actions c). As the sequence of actions a, b can be arbitrary long, the size of corresponding parallel component p is "unbounded" (i.e. for every n>0, there is a reachable state where size(p) > n). Let m be the maximum size of left-hand sides of rewrite rules in A. Further, consider the state of the form (p\\q\\s).r, where size(p) > m and process terms s, r can be e. Then there is no rule, which can change p together with some other part of the term. In other words, there is no way how can q or s provide an information to p. We need such kind of communication for the transition labelled by y, which allows to perform actions a', b', d. One possible way how to enable these actions at the same time, is to add some term I in front of the parallel composition and enable the action by removing I. But any application of a rewrite rule on the process term of the form l.(p\\q\\s).r cannot modify the process term p if p 4.2 HIERARCHY OF PRS WITH FINITE CONSTRAINT SYSTEMS__________39 is large enough. Thus we cannot add information about next possibly performed actions a, b to p (as well as I cannot be generated by p after the action x if p is large enough). In other words, the problem is that a very large parallel component (which is an sequential composition at the top-level) cannot get any information from other parallel components. Example 4.10. (sePA non-fcPRS) Let Abe a sePA system with the initial state pX\\Y and the the following rewrite rules. pX c—>- pA.X p A c—>- pA.A pB c—>- pA.B p A c—>- pe pX c—>- pB.X pA c—>- pB.A pB c—>- pB.B pB c—>- pe C C pY c—> pY\\C pC c—> pe pY^oY The system A is the same as the wPA non-fcPRS system of Example 5.29. Hence, also in this case we conjecture that there is nofcPRS system bisimilar to the considered sePA A (see Example 5.29 for more information). 40_____________________PRS WITH FINITE CONSTRAINT SYSTEMS (fcPRS) Chapter 5 Weakly Extended PRS (wPRS) The state extension of PRS, described in Chapter 3, is very naturally motivated and brings useful modelling abilities. On the other hand it is too strong at least from point view of automatic verification. State extended PA systems are able to emulate a universal Turing machine. Therefore, from model checking point of view, these systems (and those of the even more expressible classes, namely sePAN, sePAD, and sePRS) are not interesting enough because even the reachability problem is undecidable for them. In the case of BPA the state extended version coincides with previously defined class of (S, 5)-PRS systems. Hence, the only "new and interesting" class is the class of seBPP systems. Being motivated by this observation, it is worth to look for a weaker extension of PRS. Strejček has defined PRS with finite constraint systems and shown that his definition brings new classes lying strictly between each original PRS class and its non-equivalent state extended counterpart (see Chapter 4). Unfortunately, the finite constraint specification is quite complicated and so it is a bit unhandy and not so common for modelling systems of processes. In other words, it remains "too close" to its initial motivation (coming from CCP) to be useful for modelling different kind of FSU. In this chapter, we introduce yet another extension lying between the finite constraint extension and the state extension. A definition of our extension is very close to the state extension (that succeed in modelling abilities) and at the same time it keeps advantages of the finite constraint extension (esp. decidability of the reachability problem). 5.1 Definition of Weakly Extended PRS This section defines weakly extended PRS (wPRS) classes that were introduced in [KRS04b]. We extend PRS by a finite state control unit whose transition function satisfies some restrictions inspired by weak finite automata 42 WEAKLY EXTENDED PRS (wPRS) (introduced in [MSS92], but used here as a nondeterministic (NFA) rather than alternating one). Roughly speaking, weakly extended PRS is a state extended PRS where the FSU is weak (its transition function exhibits some monotonicity). Definition 5.1. Let Act = {a,b,- ■ ■} be a countably infinite set of atomic actions and ex,ß G {1,S,P,G} such that ex c ß. An (ex, /3)-wPRS (weakly extended PRS) is a tuple A = (M,>,R,mo,to), where • (M, >) is partially ordered finite set representing states of weak finite-state unit; the elements of M are called w-states, • R C ((M x (a\{e})) x Act x (M x /?)) is afinite set of rewrite rules of the form ((m, t\),a, (n, Í2)) satisfying the condition m>n. • mo G M is an initial w-state of the control unit, and • to G ß is an initial term. We write ((m,t\) ^-> (n, Í2)) G R instead of ((m, ti), a, (n, Í2)) G R. To shorten our notation we write mt instead of (m, t). As in the PRS case, instead of (mt\ c-^ nt2) G R where A = (C, R, tt, to), we usually write (mil °-*- ^2) G A. The meaning of Const(A) (process constants used in rewrite rules or in to), Act(A) (actions occurring in rewrite rules), and M (A) (values of the store occurring in A) for a given wPRS A is the same as in the sePRS case. Definition 5.2. The semantics of an (ex, ß)-zvPRS A = (M, >, R, mo, to) is given by the LTS (S, Act(A), —>&, moto), where • S = M(A) x {t G ß I Const(t) C Const(A)}, • moto is the initial state composed of the initial w-state mo and the initial term to, and • the transition relation —>a is defined as the least relation satisfying the following inference rules for all mt\, nt2, m(ii||i), m(Í2p), n(t\.t), n(t2-t) G S and a G Act (A). (mil °-*- nt2) G A mil —>a nt2 mt\ —a. nt2 mti -%\ nt2 m(či||č) -%\ nfoWt) m(t\.t) -%\ n(t2-t) Note that parallel composition is commutative and, thus, the inference rule for parallel composition also holds with t\ and t exchanged. 5.2 HIERARCHY OF WEAKLY EXTENDED PRS 43 The presented notion of weakness corresponds to 1-weakness condition in automata theory. (As we do not consider final states here, the general weak unit would coincide with standard state-extension; more precisely, all the states of M could be included in one partition block.) In any transition sequence, following the rules of R, the w-state components form a non-increasing sequence with respect to >. Hence, similarly to the finite constraint extension, the w-state is monotonie. However, in contrast to fcPRS, the weak unit can forbid the application of any rewrite rule. As this is the monotonicity is the only restriction and the FSU is finite, we can also reformulate the difference between wPRS and sePRS as follows. wPRS is a sePRS where its FSU can change its state only finitely many times during every execution. As instead of (1, S*)-sePRS, (1, P)-sePRS, etc. we use more traditional abbreviations seBPA, seBPP, etc., we also take up this notation for all weakly extended PRS classes. Thus for (1, l)-wPRS, (l,S*)-wPRS, (l,P)-wPRS, (S,S)-wFRS, (l,G)-wPRS, (P,P)-wPRS, (S,G)-wFRS, (P,G)-wPRS, and (G, G)-wPRS we use human-readable abbreviations wFS, wBPA, wBPP, wPDA, wPA, wPN, wPAD, wPAN, and wPRS respectively. 5.2 Hierarchy of Weakly Extended PRS In this section we discus relations between classes of PRS, PRS with finite constraint systems, weakly extended PRS, and state extended PRS. A hierarchy of all these systems is depicted in Figure 5.1 and called the extended PRS-hierarchy. It is an immediate observation that (a,ß)-FRS C (a,ß)-icFRS C (a, ß)-wFRS C (a,ß)-seFRS hold for every (a, /3)-PRS class (even up to isomorphism). The first and the last inclusions are obvious. To justify the second inclusion we take an arbitrary (a, /3)-fcPRS A with an initial term to and a constraint system C = (C, h, A, tt,ff). The corresponding (a, ß)-wFRS is A' = (C^{ff},>,R',tt,t0), where R' = {oil ^(oA n)Í2 | {mt\ c-^ nt2) G A and o\- m and o An ^ ff} and>=(h)"1. We also note that the classes FS, PDA, and PN have the same expressive power as the corresponding {fc,w,se} extended classes. Finally, we mention that for every two classes X and Y of PRS 44 WEAKLY EXTENDED PRS (wPRS) { se, w,ŕ c } PD A=PD A=seBR {se,w,fc}FS=FS Figure 5.1: The extended PRS-hier archy. 5.2 HIERARCHY OF WEAKLY EXTENDED PRS 45 X c Y implies wX c wY. The strictness ('C') of all relations of the extended PRS-hierarchy and incomparability of all non-related classes of the extended PRS-hierarchy follow from exemplifying the following systems: a BPP system which is not bisimilar to any PDA system, a fcBPP system which is not bisimilar to any PAD system, a wBPP system which is not bisimilar to any f cPAD system, a PPDA system which is not bisimilar to any wPAD system, a PN system which is not bisimilar to any PPDA system, a PAN system which is not bisimilar to any sePAD system, a BPA system which is not bisimilar to any PN system, a fcBPA system which is not bisimilar to any PAN system, a wBPA system which is not bisimilar to any f cPAN system, a PDA system which is not bisimilar to any wPAN system, a PAD system which is not bisimilar to any sePAN system, a fcPA system which is not bisimilar to any PRS system, a wPA system which is not bisimilar to any f cPRS system, and a sePA system which is not bisimilar to any wPRS system. For the non-bold items we simply refer to Section 2.3, Section 3.2, and Section 4.2, where the systems are exemplified. The bold systems are examined in the following subsections. Unfortunately, concerning the wPA non-fcPRS and sePA non-wPRS systems, we can speak about our conjectures only. Therefore these systems are included in the last subsection of conjectures. 46 WEAKLY EXTENDED PRS (wPRS) 5.2.1 wBPP Non-bisimilar to any f cPAD Constructing a proof of this section, we also formulate a property that forms a sufficient condition for a PAD to be bisimilar to some PDA (see the following definition and Lemma 5.6). Definition 5.3. An LIS (S, Act, —►, ao) is deadlockable if for each reachable nonterminal state a there is a transition from a to a terminal state. V a G S : ao —>* a ==> 3 a G Act, ß G S : a —► ß -/->■ A rewrite system A is deadlockable if its underlying LTS is deadlockable. Let us note that deadlockable does not mean "there is a (reachable) deadlocked state in the system". The definition says that every reachable state of the system has an immediate deadlocked successor. Definition 5.4. A sequential subterm t (i.e. t G S) of term g e G is a ready parallel component if and only if t is a maximal subtree in the syntax tree of term g such that t is not in the right-hand side subtree of any sequential node (i.e. node corresponding to sequential operator). A ready parallel component t is live in a PAD system A if t is not deadlocked (i.e. there is a rule applicable to t). The ready parallel components can be intuitively defined as the maximal sequential parts of a PAD process g such that g can perform an action a if and only if some of its ready parallel components can perform the same action a. Lemma 5.5. Every reachable state of an arbitrary deadlockable PAD system has at most one live ready parallel component. Proof. Observe that the application of a PAD rewrite rule can only modify one ready parallel component. Hence there is no way how to deadlock more than one live ready parallel component by one application of a PAD rewrite rule. D Lemma 5.6. Every deadlockable PAD system is bisimilar to a PDA system. Proof. The proof is build as a transformation of PAD rewrite rules onto corresponding PDA rewrite rules. This is sufficient as for every PAD there is a bisimilar PAD system with a single process constant as the initial process term (see Remark 2.9). There is only one way to revive a deadlocked parallel component, namely to rewrite adjacent components onto e. For example if B.C is a deadlocked ready parallel component of (A.C\\B.C).D and (A.C\\B.C).D -^U* (e\\B.C).D = B.C.D then the ready parallel component B.C.D can be live. 5.2 HIERARCHY OF WEAKLY EXTENDED PRS 47 Let A be a PAD system and X ^ Const (A) be a fresh process constant. Let us consider a rewrite rule of A with the right hand side containing a maximal subterm of the form l.(ti\\t2).r, where či, Č2 G S and I, r can be e. In an arbitrary transition sequence the components či, Č2 generated by the application of the considered rewrite rule become ready at the same time. Thus at least one of them is deadlocked. Let Č2 be deadlocked. We replace the subterm Z.(či||Č2).r of the rule by l.X.t\.X.t2-r (or just t\.X.t2-r whenever I is e). The process constant X eliminates any possible (unwanted) interaction of (the tail of) the term I and (the beginning of) the term či (or the tail of či and the beginning of Č2 respectively). Repeating this procedure eliminates all parallel operators from rewrite rules. The resulting PDA system A' enriched by rewrite rules of the form X.s °-> s' for every rule s °-> s' G A' is bisimilar to the given A. D Example 5.7. (wBPP non-fcPAD) Let A\ be the zvBPP system with the initial state pX and the rules: pX c^r pX\\A\\B pA^pe pB c-^ pe pX c-^ qe Lemma 5.8. There is no PAD system bisimilar to the zvBPP system A\ of Example 5.7. Proof. Ai is deadlockable. Due to Lemma 5.6 it suffices to prove there is no PDA system bisimilar to Ai. This directly follows from the fact that the language L generated by A1 is not context-free. More precisely context-free languages are closed under intersection with regular languages and L n {c}* {a}* {b}* {d} = {ckalbmd \0*A ms and ms is bisimilar to the initial state pX of Ai. The only transitions starting at states reachable from ms and changing the value of the store can be the transitions leading to terminal states, i.e. the transitions labelled by d. Hence we can directly assume that all rewrite rules of A labelled with x G {a, b, c} have the form (tt t\ c-^ tt Č2). Let A' be a PAD system with the set of rewrite rules as 48 WEAKLY EXTENDED PRS (wPRS) {íi ^ Í2 I (tt íi ^ řř í2) eA,j;/(í}U U {ti^ Z \(ttti^nt2) r, where (ml c—> mr) G A and v G {g, a, b, c, d}. It is obvious that this PAN system A' is bisimilar to the PPDA system defined in Example 3.4 - a contradiction. D 5.2.3 wBPA Non-bisimilar to any fcPAN Definition 5.12. A parallel subterm t (t G P \ {e}) of term g e G is a ready sequential component if and only if t is a maximal subtree in the syntax tree of term g such that t does not occur in any right sequential component of g. A ready sequential component t of term g is called non-trivial if and only if 3ť / e such that t.ť is a subterm of g (i.e. t is located in subterm t.ť of g, where ť ŕ e). Intuitively, the ready sequential components are defined as maximal parallel subterms of a fcPAN process g such that g can perform an action a if and only if some of its ready sequential components can perform the action a. Definition 5.13. Let L = (S, Act, —►, cto) be a labelled transition system, a be a state of S, S be a subset of Act, and u G S*. We define an ITS £|s to be the following restriction of C to E. (S,E,—>n(SxS x5),oo) We also define a notation onlyĽ(a, u) stating that u is a prefix of each maximal transition sequence in £|s starting in a. Definition 5.14. A sequential composition of t (i.e. the sequential operator '.' within t) is said to be accessed during a rewriting sequence from mt under w if and only if the left subterm of this sequential composition is rewritten onto e during the rewriting sequence. A sequential composition oft is called accessible from mt under w if and only if there is a rewriting sequence from mt under w such that the sequential composition is accessed during this rewriting sequence; otherwise it is called inaccessible. Definition 5.15. For every fcPAN A and every number n G No we define Kn(A) to be a set of all n-tuples (k\,k2, ■ ■ ■, kn) G Nn such that for every a,b e Act(A), a / b, every state mt of A satisfying only^a'b^(mt, aklbak2b... aknb), and every rewriting sequence from mt under aklbak2b... aknb, t includes at least n sequential compositions accessed during the rewriting sequence. 50 WEAKLY EXTENDED PRS (wPRS) Intuitively, Kn(A) is a set of all n-tuples (k\, ft2, ■ ■ ■, kn) such that each state mt of A holding the information that every run under {a, b}* starts with akl bak2 b... akn b needs at least n sequential compositions. Lemma 5.16. For every fcPAN A and every number n G No, Kn(A) / 0. Proof. We prove the lemma by induction on n. The base n = 0 is easy to prove. As every state mt and every actions a, b satisfy only^a'b^(mt,e) and every term includes zero sequential compositions accessed during an empty rewriting sequence, it holds that () G -Ko(A) for every fcPAN A. Induction hypothesis: Let n G No be such that Kn(A) / 0 for every fcPAN A. We assume the contrary for n + 1 and derive a contradiction. Let A be an fcPAN such that for every (hi,..., kn, kn+i) G Nra+1 there exist distinct actions a, b G Act (A), a state mt of A satisfying the condition only{a'b}(mt, aklb... ak"bakn+1b), and a rewriting sequence from mt under aklbak2b... aknbakn+1b such that t includes at most n sequential compositions accessed during this rewriting sequence. Due to induction hypothesis, we can choose k\,... ,kn such that (k\,...,kn) G Kn(A). Hence, for every l G N, there exist distinct actions ai, bi G Act (A), a state m\ti of the system A satisfying only^ai'bl^(miti, a^bi... a^biafoi), and a rewriting a*1bl...afnbl a\bi mti —4 m'it'i —4 mit" such that ti includes at most n sequential compositions accessed during the rewriting. Moreover, due to (k\,... ,kn) G Kn(A), ti includes exactly n sequential compositions accessed during the rewriting ai16;...ain6; mti —>*a ruß and no other sequential composition of ti is accessed during the rewriting rn'A -+\ m'{t'{ As for every l G N there is a state m\t\, we consider an infinite sequence {mft^i of these states. Let a be an infinite subsequence of the sequence {mft^i such that all states of a have the same value of the store (say m1) and the same corresponding pair of letters ai, bi (say a, b); the existence of such a subsequence follows from the finiteness of the constraint system and Act(A). We have not finished yet. There still can be a sequential composition of t[ that is accessed during the rewriting under a\bi such a composition could be created during the rewriting between ti and t[. Because of this, we 5.2 HIERARCHY OF WEAKLY EXTENDED PRS 51 differentiate between subterms of t[ depending on whether they have been changed during the preceding rewriting aklb...aknb mti —>a m>t'i • The subterms of t[ that have not been rewritten during the rewriting are called blue subterms. The new subterms of t[ that have been created (or changed) during the rewriting are called green subterms. The sequential compositions of t[ that have not been accessed during the rewriting are called blue sequential compositions. The sequential compositions of t\ that have been created during the rewriting are called green sequential compositions. Note that the green sequential compositions are exactly those inside the green subterms; the blue ones are the other, i.e. inside blue subterms and connecting blue and green subterms. The green subterms of t[ are created during at most k\ + k,2 + • • • + kn + n actions, therefore their number and syntactical lengths are bounded independently on I. In the definition of ready sequential components we described sub-terms that are significant for the next rewriting step - we disregarded the right-hand sequential components. Now, we want to focus on the rewriting sequence under a\bi. As the blue sequential components are inaccessible in the rewriting, we disregard their right-hand sequential components but the green subterms has to be included. We call this subterms interesting ready sequential components (irs-components).2 Using associativity, commutativity, and empty terms, we consider every irs-component as a parallel composition of one blue subterm and one green subterm. For example, a term ((5i || (G1.G2) || Sa || G3 ).^3) || G4 where 5i, 52, 53, B 4 are blue and G\, G 2, G s, G 4 are green, there is the the following irs-component that are composed of one blue and one green sub-term like this: (51115a) || ((Gi.G2)||G3) and (e) || (G4) also note that we can add an arbitrary number of (e) \\ (e) irs-components. Let m't'i and m't'j (i < j) be two states of a such that there is a bijection on their irs-components satisfying: the corresponding irs-components have identical green subterms and for their blue subterms Si, s j e P there is a term s e P such that Si\\s = Sj. The existence of such states follows from the bound of the number and the syntactical lengths of green subterms and due to Dickson's lemma. Besides considered the irs-components there are no other subterms of t!i rewritten during the rewriting sequence under a1 b. Hence the 2Note that irs-components are not parallel subterms they can include green sequential compositions and so they are not ready sequential components according to Definition 5.12. 52 WEAKLY EXTENDED PRS (wPRS) sequence of actions alb performed by m't^ can be performed also by m't'j. The contradiction follows from only^a'b^(mti, aklb... ak"brrb), only^a'b^(mtj, aklb... aknbaPb), and i < j. D Example 5.17. (wBPA non-f cPAN) Let us consider the following zvBPA system A3 with initial state pX. pX A p AX p A A pAA pB A pAB p A "-^ pe pX ^ pBX p A ^ pBA pB £> pBB pB "-^ pe pA c—> qe qA c—> qe pB c-^> qe qB "-^ qe In the following, actions a, b, c, d are called I-actions and actions e, / are called II-actions). Rules labelled by I-actions or II-actions are called I-rules or II-rules, respectively. States reachable from the initial state through I-actions are called I-states. Note that all I-states are nonterminal and using c and d actions can be rewritten onto a state bisimilar with the initial state. In the rest of this subsection we prove that there is no fcPAN system bisimilar to the wBPA system A3 given above. Let bis-fcPAN denote an assumed fcPAN system A bisimilar to wBPA of Example 5.17 such that I-rules of A are of the form tt t\ c-^ tt £2- Please note these rules cannot be forbidden by any value of the store. Lemma 5.18. If there is afcPAN A bisimilar to the zvBPA of Example 5.17, then bis-fcPAN A' exists. Proof. As the constraint system of A is finite it follows there exists an I-state mt of A such that each I-state reachable from mt has also m on the store (the contrary implies the infiniteness of the constraint system). As mt is an I-state, there exists a word w G {c, d}* such that mt —>*A ms and ms is bisimilar to the initial state pX of the wBPA. The system A' is derived from A as follows: s is the initial term, • the set of rules is {(tiA m)t\ ^(oA m)Í2 I nt\ °-> 0Í2 is a rule of A }, • the constraint system is restricted to the part above m, and • m is renamed tt. D 5.2 HIERARCHY OF WEAKLY EXTENDED PRS 53 Lemma 5.19. Each I-state of a Ms-fcPAN A has exactly one ready sequential component that is not deadlocked. Proof. As no I-state is deadlocked, each I-state contains at least one non-deadlocked ready sequential component. We prove that there is exactly one such a component. We assume contrary and derive a contradiction. Let t and s be two distinct non-deadlocked ready sequential components of an I-state. The are two cases. At first we assume that the I-state is non-bisimilar to the initial state. Hence, the I-state can perform e action. Let t be the ready sequential component that can perform e action. There are the following facts. • s cannot perform any I-action as the e action performed by t is not able to forbid the I-rules (i.e. to disable these actions), • s cannot perform e. Otherwise, neither s can perform enabled I-actions, nor other ready sequential component can perform them (according to the previous item with exchanged t for s), • s cannot perform / as this action is disabled in the considered state. Therefore the component s is deadlocked and we have a contradiction. Now we assume that the I-state is bisimilar to the initial state. Without loss of generality, let us assume that t can perform a action and s can perform a b action (t and s can possibly perform some other actions as well). Each possible next state has exactly one non-deadlocked ready sequential component. Thus, a action (performed by t) deadlocks or rewrites onto e term t (the action cannot deadlock or remove s) and the same effect has action b on s. Further, these actions add the ability to perform action e or / to the next state. Hence, a action performed by t changes the ready sequential component s at the same time. This is possible only if t and s are contained in the subterm of the form (t.r) \\s, where r e P \ {e} and a action rewrites t onto e: (t.r)\\s -%\ r\\s For the same reason there has to be a term r' G P \ {e} such that t and s are contained in the subterm of the form t\\(s.r'). This is a contradiction. D Definition 5.20. A ready sequential component is called dead if and only if it is non-trivial and deadlocked whenever the value of the store is tt. A left subterm of a sequential composition is called dead if and only if it contains (or is) dead ready sequential component. A sequential composition is called dead if and only of its left subterm is dead. We distinguish between a type and an instance of a ready sequential component. The type is given by (syntax of) the corresponding parallel 54 WEAKLY EXTENDED PRS (wPRS) subterm while the instance is given by the subterm together with its position within the term. If it is clear from the context, we do not specify the meaning explicitly. In what follows any dead ready sequential component occurring in some I-state of A is referred to as dead ready sequential component ofbis-fcPAN A. Lemma 5.21. Given Ms-fcPAN A, the set of types of dead ready sequential components occurring in I-states of A is finite. Proof. As a dead ready sequential component is non-trivial, it remains ready and unchanged during an arbitrary sequence of I-actions. In a bis-fcPAN, there are only two possibilities of creating a dead ready sequential component. Either it is included in the initial term, or it is on the right-hand side of an applied rule (it cannot be created by deadlocking some non-deadlocked ready sequential component as each I-state has exactly one non-deadlocked ready sequential component). Hence the lemma follows from the fact that the length of an initial term and the set of rules are both finite. D Definition 5.22. Let Abe a Ms-fcPAN and r be a dead ready sequential component of A. Then r is called • restricted for an I-state tt t of A if and only if there is no I-state with an added instance of dead ready sequential component r reachable from tt t, • multiplicative for an I-state tt t of A if and only if for each I-state tt ť reachable from tt t, there is an I-state tt t" reachable from tt ť such that there are more instances of r in mt" than in mť (i.e. arbitrary many instances of r can be added). We call an I-state tt tdr of A dead-restricted if and only if every dead ready sequential component of A is either restricted, or multiplicative for tt tdr- Lemma 5.23. Let Abe a Ms-fcPAN. There is a dead-restricted state tt tdr of A reachable from the initial state. Proof. If every dead ready sequential component of A is either restricted, or multiplicative in an I-state tt t then the tt tdr is found. Otherwise, there is a dead ready sequential component r such that it is neither restricted, nor multiplicative. As r is not multiplicative for tt t, there is an I-state tt ť reachable from tt t such that every I-state reachable from tt ť has the same number of instances of r as tt ť. Hence, r is restricted for the I-state tt ť. Compared to tt t, at least one more type of dead ready sequential component is restricted. Due to Lemma 5.21, we can find tt tdr by applying this procedure finitely many times. D 5.2 HIERARCHY OF WEAKLY EXTENDED PRS 55 Lemma 5.24. Given í e N, bis-fcPAN A, and dead-restricted state tt tdr, there is a dead-restricted state t^j, of A reachable from the state tt tdr such that rd%l includes at least i instances of each multiplicative dead ready sequential component. Proof. This lemma is a straightforward consequence of the definition of multiplicative dead ready sequential components. D In what follows, by a sequential composition is behind a subterm s in term r we mean that, in the term r, s is included in the left subterm of the sequential composition. By a subterm t is behind a subterm s in term r we mean that there is a sequential composition in the term r such that t is included in the left subterm and s is included in the right subterm of this sequential composition. Lemma 5.25. If there are more than í instances of dead ready sequential component r in a state tt t of a bis-fcPAN, then all the sequential compositions behind these instances are inaccessible from tt t under any sequence of the form eklfek2f ... ekn f such that n G No and k j < í for every 1 < j < n. Proof. We assume the contrary and derive a contradiction. Let tt t be a state of a bis-fcPAN with more than i instances of some dead ready sequential component such that a sequential composition behind some of these instances is accessible under eklfek2 f ... eknf. The definition of bis-fcPAN implies that only^e'^(tt t, ekl fek2 f... ek"f) holds. From the definition of fcPAN, it follows that a rule which has been already used cannot be forbidden in future. Thus, whenever an action is performed by one of the instances, the same rule can be immediately applied on the other instances. Hence, a coherent sequence of more that i actions with the same label can be performed. This is a contradiction with only^'^ (tt t,eklfek2f... ekn /). D Lemma 5.26. There is nofcPAN system bisimilar to the wBPA of Example 5.17. Proof. Lemma 5.18 implies that it is sufficient to show that there is no bis-fcPAN. For the sake of contradiction, let us assume that there is a bis-fcPAN system A with an initial term to and a set of constraints C. Let us consider the following transition sequence: tt to —+*A tt tdr —& tt 4? ^A it r The state tt tdr is a dead-restricted state (its reachability follows from Lemma 5.23). Let I be the number of sequential compositions in tdr and n = I + \C\ + 1. Lemma 5.16 implies that Kn(A) is non-empty. Let (fci, &2,..., kn) G Kn(A) and k be the maximum of fe, &2, • • •, kn. Then (k) tt tdr denotes the dead-restricted state with more than k instances of each multiplicative dead ready sequential component (it is reachable due to Lemma 5.24). Further, wn = bak" ... bak2bakl. 56 WEAKLY EXTENDED PRS (wPRS) The term r is a non-deadlocked term, hence it can be written in the form (' ' ' ((((((' ' ' ((((í.íl)ll*l).Í2)||*2) ' ' ' •tn)\\8n).7)\\5).T')\\5') • • • .7(m))P(m), where ieP\ {e} is the only one non-deadlocked ready sequential component (Lemma 5.19), and či,..., tn, s\,..., sn, 7,..., ^m\ 5,..., ö^ G G. As e G G, this form says only that the term č is a ready sequential component in an arbitrary position of r. As (ki,..., kn) G Kn(A) and only^c'd^((ttr, chld... ch"d) then r includes at least n sequential compositions accessed (see Definition 5.14) during the rewriting sequence from tt r under ckld... cknd. Let us assume that či,..., tn-i G P for now. If Si includes a sequential composition then Si includes a non-trivial ready sequential component. According to Lemma 5.19, this non-trivial ready sequential component is deadlocked. Hence Si includes a dead ready sequential component and all sequential compositions behind this component are dead. This means that the compositions are inaccessible under ckld... cknd. Thus at most i — 1 sequential compositions are accessed under I-actions. This is less than n and so it contradicts the property obtained in the previous paragraph. Hence si,..., sn-i G P, č, či,..., čra_i G P \ {e}, and all dead ready sequential components of r are included in subterms ö,...,ö^m\ Further, similarly to the sequential compositions of Si discussed above, all the sequential compositions of 5,..., 5^ are dead. From Lemma 5.19 it follows that ti\\si (where 1 < i < n) is a new ready sequential component appeared by accessing the i-th sequential compositions. If U includes a sequential composition then it is not necessary to access all the compositions down to tn - those of U (i < n) will be accessed instead. A sequential composition in tí also implies that tí includes a non-trivial ready sequential component. This ready sequential component will be a proper subterm of ti\\si appearing by accessing the sequential composition before U. As (k\,..., kn) G Kn(A) and only^e'f^(tt r,eklf... eknf), r includes at least n sequential compositions accessed during the rewriting sequence from tt r under eklf...eknf. We recall that all dead sequential compositions are in 6,...,6^. From Lemma 5.25 it follows that all the sequential compositions behind a multiplicative dead ready sequential components are inaccessible. Hence, the only accessible sequential compositions of 6,..., 5^ are behind restricted dead ready sequential components. According to the definitions, all restricted dead ready sequential components and the terms behind them have already been created in tdr. Hence, there are at most I such accessible compositions in r. Thus at least \C\ + 1 (= n — I) sequential compositions 5.2 HIERARCHY OF WEAKLY EXTENDED PRS________________________57 of the subterm ((• • • ((č.či)||si) • • • .tn)\\sn) are accessed during a rewriting sequence from tt r under eklf...eknf. If there is U (i < \C\ + 1) with a sequential composition, then accessing the i-th composition "creates" the same ready sequential composition that appears as in the rewriting sequence under ckld... cknd. Hence, a I-action can be performed and we derived a contradiction. Therefore, či, • • • ,č|c|+i S P and all the sequential compositions of ((• • • ((č.či)||si) • • • -í|c|+i)lls|c|+i) are accessed during the sequence under eklf.. .eknf. For every 1 < i < \C\ + 1, accessing the i-th composition have to be preceded by changing sf, otherwise we get the same ready sequential component čí 11Si as in the rewriting sequence under ckld... cknd and I-actions can be performed. The only possibility of forcing the preceding is to change the store during at least one action performed by s». Otherwise all the actions performed by Si can be omitted without any effect on the rewriting sequence accessing the i-th composition. Hence we have to change a constraint at least \C\ + 1 times. It is the contradiction and Lemma 5.26 is proved. D 5.2.4 PDA Non-bisimilar to any wPAN system of Exam- U.A.B U.B.B V.B W.B V >w but having U.X.Y as the initial state and being extended with the following two rewrite rules: V.Y A U.X.Y W.Y A U.X.Y This system, denoted by A4, behaves like that defined in Example 2.13, but whenever the original system terminates, the enhanced A4 is restarted under the action x. Lemma 5.28. There is no wPAN A bisimilar to the PDA A4 of Example 5.27. Proof. The proof is similar to the proof of Lemma 5.11 using the fact the PDA of Example 2.13 is not bisimilar to any PAN system. To derive a contradiction assume a wPAN A bisimilar to the PDA A4. As the weak state unit of A is finite then there exists a reachable state mt Example 5.27. (PDA non-wPAN) Let us consider a PDA pie 2.13 U.X ^ U.A.X U.A A U.A.A U.B A U.X <\ U.B.X U.A <\ U.B.A U.B <\ U.X A V.X U.A A V.A U.B A U.X ^ W.X U.A ^ W.A U.B ^ V.X ^V V.A^V V.B ^ W.X ^ W W.A A W W.B ^ 58 WEAKLY EXTENDED PRS (wPRS) of A such that every state reachable from mt has also m as its w-state component (the opposite would imply the infiniteness of the weak state unit). There exists a word w G {a, b, c, d, e, /}* such that mt ^%*A mť, where mt' is bisimilar to the state U.X.Y of the PDA process A4. If the rules labelled by the action x are removed from A and mt' is taken as the initial state, we obtain the system whose all reachable states have m as w-state component and which is bisimilar to the pushdown process of Example 2.13. Now let A' be a PAN system with the initial state ť and with the set V V of rewrite rules consisting of the rules I c—> r, where (ml c—> mr) G A and v G {a, b, c, d, e, /}. It is obvious that this PAN system A' is bisimilar to the PDA system defined in Example 2.13 - a contradiction. D 5.2.5 Intuition and Conjectures To accomplish the strictness/incomparability proof it remains to show a wPA non-fcPRS system and an sePA non-wPRS system. We conjecture that the following two systems exemplify the desired systems. Example 5.29. (wPA non-f cPRS) Let Abe a wPA system with the initial state pX\\Y and the the following rewrite rules. pX c—>- pA.X p A c—>- p A. A pB c—>- pA.B p A c—>- pe pX c—>- pB.X pA c—>- pB.A pB c—>- pB.B pB c—>- pe C C pY c—> pY\\C pC c—> pe pY^oY We conjecture that there is nofcPRS system bisimilar to this wPA A. This system is composed of two subsystems running in parallel. The fist subsystem is a stack with "push" actions a, b and "pop" actions a', b'. The second subsystem forms a counter with an increment action c and a decrement action é'. Due to the rule with a label d, the system is deadlockable (see Definition 5.3). It is easy to see that for every reachable non-deadlocked state a, there is a sequence of actions w G {a', b', c'}* such that a —>* ß and ß is bisimilar to the initial state. Hence, similarly to Lemma 5.18, we can assume, without loss of generality, that a desired fcPRS system has all x G {a, b, c, a', b', c'} rules of the form tt *i A řř Í2. Let us note that these rules cannot be forbidden by any value of a finite constraint store. Assume an fcPRS system A' bisimilar to the wPA A of Example 5.29. Therefore, the system A' can perform an unbounded number of c actions. 5.2 HIERARCHY OF WEAKLY EXTENDED PRS 59 An execution of arbitrary large number of c actions leads to a state from where exactly the same number of d actions can be performed. This "unbounded" number has to be saved in a possibly very large term inducing the d actions; let us call this term the counter. Now, let us execute a very long sequence of a and b actions, an achieved state has to store this sequential information. Hence, a long sequence of sequential components forms a stack in the term part. While building this stack, it is impossible to carry the long "counter" subterm on the top of this stack. Hence, the "counter" term (inducing d actions) and the top of the stack (inducing a sequence of a' and b' actions) are far away from each other (at any arbitrary distance), and so they cannot be both changed during one rewriting step. This is a contradiction with a deadlockable property and the type of all a, b, c, a',b', d rules. Example 5.30. (sePA non-wPRS) Let Abe a sePA system with the initial state pX\\Y and the the following rewrite rules. pX ^ pA.X pA ^ pA.A pB< ^pA.B p A <-^f pe pX ^ pB.X pA ^ pB.A pB< -^pB.B V pB "-^ pe pY^pY\\C pC c-^ pe pY^oY oA c—> oe oB c—> oe oC< e —> oe oX^pX We conjecture that there is no wPRS system bisimilar to this sePA A. In this system the actions a,b,c,a',b',d and d work in the same way as in the previous example. Moreover, after performing an action d the system is not deadlocked but the counter and the stack can be "discharged" using e actions and then an action / can "restart" the system. In other words, for every reachable state a, there is a sequence of actions w e {d, e, /}* such that a —>* ß and ß is bisimilar to the initial state. Assume a wPRS system A' bisimilar to the sePA A of Example 5.30. As the weak state unit of A' is finite, there exists a reachable state mt of A' such that every state reachable from mt has also m as its w-state component (the opposite would imply the infiniteness of the weak state unit). As every execution of A' can be prolong to reach a state bisimilar to the initial state, we can obtain a wPRS system whose all reachable states have the same w-states. Therefore, we derived that there is also a PRS system A" bisimilar to the system A'. Removing all rewrite rules with the label e and all rewrite rules with the label / from the PRS system A" we create a PRS system bisimilar to the wPA non-fcPRS system of Example 5.29. This is a contradiction with our previous assumption. 60___________________________________WEAKLY EXTENDED PRS (wPRS) Chapter 6 Strong Bisimulation Equivalence In this chapter we focus on (un)decidability as well as complexity boundaries on strong bisimilarity between two states of a given extended PRS. Concerning this research area we have not reach any new results, therefore we only summarises all known results and briefly mention what we have tried to do and where our attempt has failed. 6.1 Motivation Equivalence checking is one of the main streams in verification of concurrent systems. It aims at demonstrating some semantic equivalence between two systems, one of which is usually considered as representing the specification, while the other as its implementation or refinement. The semantic equivalences are designed to correspond to the system behaviours at the desired level of abstraction; the most prominent ones being strong and weak bisimulations. We mention some results on equivalence checking with strong bisimilarity here. The weak bisimilarity is discussed in the next chapter. For the other equivalence checking problems we refer to surveys [BCMS01, Srb04] for example. The bisimilarity problem for BPA is known to be in 2-EXPTIME [BCS95] and PSPACE-hard [Srb02c]. The first result showing that the bisimilarity problem for PDA is decidable was published in [Sén98]. Later on, bisimilarity was determined to be EXPTIME-hard for PDA [KM02]. EXPTIME-hardness is also the best known lower bound for the PAD, fcPAD, and wPAD classes where, moreover, the decidability left open. Considering the parallel systems, the strong bisimilarity problem is un-decidable for seBPP (also known as PPDA) [Mol96] using the technique introduced in [Jan95b]. However, the strong bisimilarity is known to be decidable for BPP [CHM93]. Moreover, it was shown that the problem 62 STRONG BISIMULATION EQUIVALENCE belongs to PSPACE [Jan03]. Combining with PSPACE-hardness result of [Srb02b], PSPACE-completeness was established. The result of [Srb02b] (PSPACE-hardness for BPP) presents also the best known lower bounds for bisimilarity for PA, fcPA, wPA, fcBPP, and wBPP, but in these cases, contrary to BPP, the decidability of bisimilarity left open. 6.2 Definition of Strong Bisimilarity Bisimilarity was originally introduced by Park [Par81] and Milner [Mil89]. Definition 6.1. A binary relation R on set of states S is a strong bisimulation if and only if for each (a, ß) G R the following conditions hold: • Va'e5,oe4ci:aA«' implies (3/3' eS:/?A/3'A (a', ß') G R) • V/3' G S, a G Act : ß -^ ß' implies (3a' e S :a^a' A (a', ß') G R) States a and ß are strongly bisimilar, written a ~ ß, if and only if (a, ß) G R for some strong bisimulation R. Two labelled transition systems are strongly bisimilar if and only if its initial states are strongly bisimilar. Problem: Strong bisimilarity problem for an extended (a, ß)-PRS class Instance: An extended (a, /3)-PRS system A and two of its states mt, m'ť Question: Are the two states mt and m'ť strongly bisimilar? 6.3 Summary As we have mentioned in Section 6.1, the problem for BPP is in PSPACE but it is undecidable for the state extended variant (seBPP). This encouraged us to focus on the strong bisimilarity problem for wBPP staying in between these two classes. We tried to prove the problem is decidable. The crucial difference between BPP and wBPP is as follows. It is known that the following congruence holds for every parallel terms t\, t2, Í3, and Í4 of a BPP system. Í1 ~ Í2 A Í3 ~ Í4 => íi||Í3 ~ Í2||Í4 But in the context of wBPP systems pt\ ~ pt2 does not imply either pt\ \\t ~ pt2 \\t. This can be shown e.g. by the following example. Example 6.2. Let A be a wBPP with the following rewrite rules. 6.3 SUMMARY 63 p A <-^f pe pB <—> qs qC <—> qC It is easy to see that pA~pB A pA\\C tL pB\\C. This behaviour of wBPP systems counterwork all our attempts to adopt known proves for BPP such as a tableau decision method [CHM93] or a DD-f unction characterisation [Jan03]. Therefore the decidability of bisim-ilarity problem for wBPP left open. Figure 6.1 shows (un)decidability borders of strong bisimilarity problems. 64 STRONG BISIMULATION EQUIVALENCE sePRS sePAN und ecid able decidable _._ sc PDA PPDA und ecid able decidable Figure 6.1: The extended PRS-hierarchy with (un)decidability boundaries of strong bisimilarity. Chapter 7 Weak Bisimulation Equivalence Weak bisimilarity is one of the most studied behavioural equivalences. This equivalence is undecidable for pushdown processes (PDA), process algebras (PA), and parallel pushdown processes (PPDA). Its decidability is an open question for basic process algebras (BPA) and basic parallel processes (BPP). We move the undecidability border towards these classes by showing that the equivalence remains undecidable for weakly extended versions of BPA and BPP. In fact, we show that the weak bisimulation equivalence problem is undecidable even for normed subclasses of BPA and BPP extended with finite constraint systems. 7.1 Motivation Weak bisimulation equivalence is one of the semantic equivalences with a silent action. These equivalences are based on a notion of observable behaviour of systems: only the interactions of the system with the environment (observer) are observable. The internal structure of the system is not considered observable and system internal activities are modelled by silent (r) actions which can precede and/or follow any observable action. For an overview of equivalences with silent moves and more general setting with respect to various testing scenarios we refer to [vG93]. Now, we mention some of the results on checking with weak bisimulation equivalence (bisimilarity). Regarding sequential systems, i.e. those without parallel composition, the weak bisimilarity problem is undecidable for PDA even for the normed case [Srb02d]. However, it is conjectured [May05] that weak bisimilarity is decidable for basic process algebras (BPA); the best known lower bound is EXPTIME-hardness [May05]. Considering parallel systems, even strong bisimilarity is undecidable for parallel pushdown processes as shown in (PPDA) [Mol96] using the tech- 66 WEAK BISIMULATION EQUIVALENCE nique introduced in [Jan95b]. However, it is conjectured [Jan03] that the weak bisimilarity problem is decidable for basic parallel processes (BPP); the best known lower bound is PSPACE-hardness [Srb03a]. For the simplest systems combining both parallel and sequential operators, called PA processes [BW90], the weak bisimilarity problem is unde-cidable [Srb03b]. It is an open question for the normed PA; the best known lower bound is EXPTIME-hardness [May05]. In this chapter, we move the undecidability border of the weak bisimilarity problem towards the classes of BPA and BPP, where the problem is conjectured to be decidable. Section 7.3 contains (relatively simple) proofs of undecidability of the considered problem for the weakly extended versions of BPA (wBPA) and BPP (wBPP). In Section 7.4, we strengthen the results by showing that even for more restricted systems, namely for normed fcBPA and normed fcBPP systems, this equivalence remains undecidable. In fact, the result is not new for wBPA due to the following reasons: Mayr [May05] has shown that adding a finite-state unit with 2 states (i.e. of the minimal non-trivial size) to a BPA process already makes weak bisimilarity undecidable. Our inspection of his proof shows that a finite state unit used in the proof is weak and so the result is valid for wBPA as well. 7.2 Definition of Weak Bisimilarity It is common to admit silent transitions to model the internal unobserv-able evolution of a system. In standard automata theory these are typically referred to as "epsilon" transitions, but in concurrency theory they are commonly represented by a distinguished action r G Act. Definition 7.1. Let (S, Act, —►, ao) be an LIS and r G Act be a distinguished action. A relation of observable transitions ==> c (S x Act x S) is defined as follows: a =^=> ß if and only if a —>* ß where w G {r}* a =^=> ß if and only if a —>* ß where w G {r}* • {a} • {r}* and a / r. We also use a natural generalisation a =^=> ß for finite sequences w G Act*. Definition 7.2. A binary relation R on set of states S is a weak bisimulation if and only if for each (a, ß) G R the following conditions hold: V a' eS,aeAct:a^a' implies (3ß' G S : ß =^ ß' A {a1, ß1) G R) • V/3' G S, a G Act : ß -^ ß' implies (3a' G S : a =^ a' A (a', ß') G R) States a and ß are weakly bisimilar, written a w ß, if and only if (ex, ß) G R for some weak bisimulation R. Two labelled transition systems are weakly bisimilar if and only if their initial states are weakly bisimilar. 7.3 UNDECIDABILITY OF WEAK BISIMILARITY 67 We use a characterisation of weak bisimilarity in terms of a bisitnulation game, see e.g. [Sti96]. This is a two-player game between an attacker and a defender played in rounds on pairs of states of a considered labelled transition system. In a round starting at a pair of states (ct\, a-i), the attacker first chooses i G {1,2}, an action a e Act, and a state oli such that ckj —► c^. The defender then has to choose a state a^ such that as-i ==> a^.j. The states a[, a'2 form a pair of starting states for the next round. A play is a maximal sequence of pairs of states chosen by players in the given way. The defender is the winner of every infinite play. A finite game is lost by the player who cannot make any choice satisfying the given conditions. It can be shown that two states cti,ct2 of a labelled transition system are not weakly bisimilar if and only if the attacker has a winning strategy for the bisimulation game starting in these states. We study the following problems for extended (a, /3)-PRS classes. Problem: Weak bisimilarity problem for an extended (a, ß)-PRS class Instance: An extended (a, /3)-PRS system A and two of its states mt, m'ť Question: Are the two states mt and m'ť weakly bisimilar? 7.3 Undecidability of Weak Bisimilarity In this section, we show that weak bisimilarity is undecidable for the classes wBPA and wBPP 7.3.1 wBPA In [May05] Mayr studied the question of how many control states are needed in a pushdown automaton to make weak bisimilarity undecidable. Theorem 7.3 ([May05], Theorem 29). Weak bisimilarity is undecidable for pushdown automata with only 2 control states. The proof is done by a reduction of Post's correspondence problem to the weak bisimilarity problem for PDA. The constructed pushdown automaton has only two control states, p and q. Quick inspection of the construction shows that the resulting pushdown automata are in fact wBPA systems as there is no transition rule changing q to p and each rule has only one process constant on the left hand side. Hence Mayr's theorem can be reformulated as follows. Theorem 7.4. Weak bisimilarity is undecidable for wBPA systems with only 2 control states. 68 WEAK BISIMULATION EQUIVALENCE 7.3.2 wBPP We show that the non-halting problem for Minsky 2-counter machines can be reduced to the weak bisimilarity problem for wBPP. First, let us recall the notions of Minsky 2-counter machine and the non-halting problem. A Minsky 2-counter machine, or a machine for short, is a finite sequence N= h:h, h- Í2, <>n—l ■ ^n—1, ln: halt where n > 1, h, I2, ■ ■ ■ ,ln are labels, and each i j is an instruction of one of the following forms: • increment: Cfc: = Cfc+l; goto lr • test-and-decrement: if Cfc>0 then c^ : = c^ -1; goto lr else goto ls where Ck are counters, k e {1,2}, and 1 < r, s < n. The semantics of a machine N is given by a labelled transition system. The states are configurations of the form (lj, v\, V2) where Ij is a label of an instruction to be executed and v\, V2 are nonnegative integers representing current values of counters ci and C2, respectively. The transition relation is the smallest relation satisfying the following conditions: if i j is an instruction of the form ci: = ci+l; goto lr, then (lj, v\,V2) ^>{lr,vi + 1,^2) forallvi,V2 > 0; • if ci>0 then ci: = ci-l; goto lr else goto ls, then (lj,vi + 1,^2) -^ (lr,vi,V2) for aYLvi,V2 > 0 and (lj, 0, V2) z-^ (h, 0, V2) for all V2 > 0; and the analogous condition for instructions manipulating C2. We say that the (computation of) machine N halts if there are numbers v\,V2 > 0 such that (h,0,0) —>* (ln, v\, V2). Let us note that the system is deterministic, i.e. for every configuration there is at most one transition leading from the configuration. The non-halting problem is to decide whether a given machine N does not halt. The problem is undecidable [Min67]. Let us fix a machine N = l\: i\, I2 : %2, ■ ■ ■, ln-i '■ in-i, In '■ halt. We construct a wBPP system A such that its states 7.3 UNDECIDABILITY OF WEAK BISIMILARITY 69 simLi and simL^ are weakly bisimilar if and only if N does not halt. Roughly speaking, we create a set of wBPP rules allowing us to simulate the computation of N by two separate sets of terms. If the hal t instruction is reached in the computation of N, the corresponding term from one set can perform the action halt, while the corresponding term from the other set can perform the action halt'. Therefore, the starting terms are weakly bisimilar if and only if the machine does not halt. The wBPP system A we are going to construct uses five control states, namely sim, check i, check'ľ, check2, check'2. We associate each label lj and each counter ck with process constants Lj,L'j and Xk,Yk respectively. A parallel composition of x copies of Xk and y copies of Yk, written X%\\Y£, represents the fact that the counter ck has the value x — y. Hence, terms simLjWX^W^WX^WY^2 and simL'jWX^W^WX^WY^2 are associated with a configuration (Ij, x\ — y\, X2 — 2/2) of the machine N. Some rules contain auxiliary process constants. In what follows, ß stands for a term of the form ß = X^WY^WX^WY^2. The control states checkk, check'k for k G {1,2} are intended for testing emptiness of the counter ck. The only rules applicable in these control states are: check\X\ "-^ check\£ check2X2 c-^ check2£ check'{Y\ c-^ checkte check'2Y2 °-> check'2e One can readily confirm that checkkß ~ check'kß if and only if the value of Cfc represented by ß equals zero. In what follows we construct a set of wBPP rules for each instruction of the machine N. At the same time we argue that the only chance for the attacker to win the bisimulation game is to simulate the machine without cheating as every cheating can be punished by the defender's victory. Therefore this attacker's strategy is winning if and only if the machine halts. Halt: ln: halt Halt instruction is translated into the following two rules: halt . halt' svmLn c—> svme svmLn c—> svme Clearly, the states simLn\\ß and simL'n\\ß are not weakly bisimilar. Increment: lj : ck : = c^+l; goto lr To each such an instruction of the machine N we add to A the following rules: simLj "-^ simLr\\Xk simL'j ^-> simL'r \\Xk 70 WEAK BISIMULATION EQUIVALENCE Obviously, every round of the bisimulation game starting at states simLj \\ß and simL'jWß ends up in states simLr\\Xk\\ß and simL'r\\Xk\\ß. Test-and-decrement: Ij'-if Cfc>0 then Cfc: = Cfc-l; goto lr else goto ls To each such an instruction of the machine N we add to A two sets of rules, one for the c^ > 0 case and the other for the c^ = 0 case. The wBPP formalism has no power to rewrite a process constant corresponding to a label lj and to check whether c^ > 0 at the same time. Therefore, in the bisimulation game it is the attacker who has to decide whether c^ > 0 holds or not, i.e. whether he will play an action dec or an action zero. We show that whenever the attacker tries to cheat, the defender can win the game. At this point our construction of wBPP rules uses a variant of the technique called defender's choice [JS04]. In a round starting at the pair of states cki, CK2, the attacker is forced to choose one specific transition (indicated by a wavy arrow henceforth). If he chooses a different transition, say ctk —> a where k G {1,2}, then there exists a transition as-k —> a that enables the defender to reach the same state and win the play The name of this technique refers to the fact that after the attacker chooses the specific transition, the defender can choose an arbitrary transition with the same label. These transitions are indicated by solid arrows. The dotted arrows stands for auxiliary transitions which compel the attacker to play the specific transition. First, we discuss the following rules designed for the case when c k > 0. -r dec a -a dec dec . .. svmLj c—> svmAk^r simA^r c—> cheeky simBk,r c—> simLr\\Yk t dec . dec . ,-/,,-,, . „ dec . ,-/,,-,, svmLj c—> simBk,r simA^j. c—> svmLr\\Yk sirring c—> simLr\\Yk t i dec . . dec . dec . svmLj c—> simAk^r simA^j. c—> cneckke sirring c—> cneckke simL'j "-^ simBkr simCk,r ^ simL'r\\Yk simL'j "-^ simCk,r simCk,r ^ check'ke The situation is depicted in Figure 7.1. Let us assume that in a round starting at states simLj\\ß, simL'-\\ß the attacker decides to perform the action dec. Due to the principle of defender's choice employed here, the attacker has to play the transition simL'jWß —>a simCk,r\\ß, while the defender can choose between the transitions leading from simLj\\ß either to simAk^Wß or to simBk^Wß- Thus, the round will finish either in states simAk^Wß, simCk,r\\ß or in states simBkyr\\ß, simCktr\\ß- Using the defender's choice again, one can easily see that the next round ends up in checkkß or simLr\\Yk\\ß, and simL'r \\Yk\\ß 7.3 UNDECIDABILITY OF WEAK BISIMILARITY 71 simLj simAk checkkß simLr\\Yk\\ß simĽ- dec simBkrl dec '■-. dec' x ^ simL'r\\Yk\\ß check'kß Figure 7.1: Decrement actions simulating a test-and-decrement instruction. or check'kß. The exact combination is chosen by the defender. The defender will not choose any pair of states where one control state is sim and the other is not as such states are clearly not weakly bisimilar. Hence, the two considered rounds of the bisimulation game end up in a pair of states either simLr\\Yk\\ß, simL'r\\Yk\\ß or checkkß, check'kß. The latter pair is weakly bisimilar if and only if the value of ck represented by ß is zero, i.e. iff the attacker cheats when he decides to play an action dec. This means that if the attacker cheats, the defender wins. If the attacker plays the action dec correctly, the only chance for either player to force a win is to finish these two rounds in states simLr\\Yk\\ß, simL'r\\Yk\\ß corresponding to the correct simulation of an test-and-decrement instruction with a label lj. Now, we focus on the following rules designed for the ck = 0 case: • t zero ■ n simLj "-^ simEktS ■ Tl zero ■ n ' simLj c—> simDks ■ Tl Zer° ■ TP simLj c—> simLk^g . zero simLj "-^ simFk,s simDks c-^ checkkE simDks c-^ simL'g simDks c-^ simGk ■ TP ' Zer0 ■ Tl simLk^g c—> simLg ■ T? ' ZeT0 ■ n simbks c—> simGk simEj,yS "-^ simLg ■ TP ' Zer0 ■ TI simbks c—> simLs simEj,yS "-^ simGk simGk °-*- simGk\\Yk simGk c-^ check'kYk The situation is depicted in Figure 7.2. Let us assume that the attacker decides to play the action zero. The defender's choice technique allows the defender to control the two rounds of the bisimulation game starting at states simLj\\ß and simL'j\\ß. The two rounds end up in a pair of states simLs\\ß, simL's\\ß or in a pair of the form checkkß, check'kY™\\ß where m > 1; all the other choices of the defender lead to his loss. As in the previous case, the latter possibility is designed to punish any possible attacker's cheating. The attacker is cheating if he plays 72 WEAK BISIMULATION EQUIVALENCE simLj checkkß simĽ4 simEkJ simFk ■^ h simLa simL{ simGk\ check'kYkm\ Figure 7.2: Zero actions simulating a test-and-decrement instruction. the action zero and the value of ck represented by ß, say vk, is positives In such a case, the defender can control the two rounds to end up in states checkkß, check'kY'kUk \\ß which are weakly bisimilar. If the attacker plays correctly, i.e. the value of ck represented by ß is zero, then the defender has to control the two discussed rounds to end up in states simLs\\ß, simL's\\ß as the states checkkß, check'kY™\\ß are not weakly bisimilar for any m > 1. To sum up, the attacker's cheating can be punished by defender's victory. If the attacker plays correctly, the only chance for both players to win is to end up after the two rounds in states simLs\\ß, simL's\\ß corresponding to the correct simulation of the considered instruction. It has been argued that if each of the two players wants to win, then both players will correctly simulate the computation of the machine N. The computation is finite if and only if the machine halts. The states simL\ and simL^ are not weakly bisimilar in this case. If the machine does not halt, the play is infinite and the defender wins. Hence, the two states are weakly bisimilar in this case. In other words, the states simL\ and simL^ of the constructed wBPP A are weakly bisimilar if and only if the Minsky 2-counter machine N does not halt. Hence, we have proved the following theorem. Theorem 7.5. Weak bisimilarity is undecidable for zvBPP systems. :We do not have to consider the case when ß represents a negative value of cfc as such a state is reachable in the game starting in states simLi, simL'x only by unpunished cheating. 7.4 WEAK BISIMILARITY FOR MORE RESTRICTED CLASSES 73 7.4 Weak Bisimilarity for More Restricted Classes Here, we strengthen the results of the previous section. We will show that weak bisimilarity remains undecidable for both fcBPP and fcBPA systems. Definition 7.6. An (a, ß)-fcPRS A is normed in a state moto of A if and only if for all states mt satisfying moto —>*A mt, it holds that mt —>*A oe for some o G C(A). Moreover, we show that weak bisimilarity remains undecidable even for their respective normed versions (i.e. if, in an instance of the weak bisimilarity problem, a given fcBPP/fcBPA system is normed in both given states). Hence, we show that weak bisimilarity is undecidable for normed wBPP and normed wBPA as well. 7.4.1 Normed fcBPP In this subsection, we show that weak bisimilarity is undecidable for normed fcBPP systems. Let A be the wBPP system constructed in Subsection 7.3.2. We recall that given any fixed Minsky machine N, we have constructed a wBPP system A such that its states simL\ and simL\ are weakly bisimilar if and only if N does not halt. Based on A, we now construct a fcBPP A' and two of its states simLi \\D and simlJ1 \\D such that they satisfy the same condition as given in the previous paragraph and moreover A' is normed in both of the states simL\\\D and simL^D. Let Const(A') = {D} U Const(A) and Act(A') = {norm} U Act (A), where D g" Const(A) is a fresh process constant and norm g" Act (A) is a fresh action. The constraint system of A' is depicted in Figure 7.3. checki cheeky check2 check'2 Figure 7.3: The constraint system of A'. The set of rewrite rules of A' consists of all the rewrite rules of A and 74 WEAK BISIMULATION EQUIVALENCE moreover the following rules are added: ,-1 „ norm, , , „ (1) UD ^ delD, (2) delX ^ dele for all X G Const(A'), (3) delX A delX for all X G Const(A') and a G Act (A). The process constant D enables the norm action changing the value of the store onto del. Starting in the state simL\\\D or simL'-A\D, every reachable state includes the process constant D or the current value of the store has been already changed onto del. Whenever the value of the store is set to del, the rules of type (2) can be used to make the state normed. Hence, A' is normed in both of the states simL\ \\D and simL^ \\D. It remains to show that these new rules do not affect the bisimula-tion game. Let us note that del h m and del A n ^ ff for every m, n G {tt, sim, checki, cheeky, check2, check'2}. Therefore, changing the store to del value does not forbid an application of the A rules - those with a label inc, dec, zero, chk\, etc. But the rewrite rules of the type (3) cause that using of the norm action in the game leads into weakly bisimilar states without respect to an application of the A rules. As the attacker can only decide to perform the norm action, this reconstruction of A onto A' does not change the winning strategies discussed in Subsection 7.3.2. Hence the Theorem 7.5 can be strengthen as follows. Theorem 7.7. Weak bisimilarity is undecidable for normed fcBPP systems. 7.4.2 Normed fcBPA In this subsection, we show that the problem remains undecidable for the case of normed fcBPA systems. Our proof is a slightly extended translation of the proof for PDA of [May05] into fcBPA framework. We used the notation of [May05] to make the proofs comparable. Our proof (as well as Mayr's one) is based on a reduction of Post's correspondence problem, which is known to be undecidable [HU79]. Problem: Post's correspondence problem (PCP) Instance: A non-unary alphabet X and two ordered sets of words A = {v,\,..., un} and B = {v\,..., vn} where Ui, Vi G S+ Question: Do there exist finitely many indices i\,... ,im G {1,..., n} such that uh ... uim = vh ... vim? Given any instance of PCP we now construct a normed fcBPA A and two of its states pTB, pT'B such that pTB and pT'B are weakly bisimilar if and only if the instance of PCP has a solution. 7.4 WEAK BISIMILARITY FOR MORE RESTRICTED CLASSES 75 A constraint system of A contains elements 11, p, checki, check2, del, and ff that are ordered as follows. We use process constants T,T',T1,T[,T2,T2',Gi,Gr, B and Ui,Vif for each 1 < i < n. Actions of A are a, b, c, r, norm, 1,..., n, and the letters of E. In what follows, U stands for a sequential term of process constants of {Ui | 1 < i < n} and similarly V stands for a sequential term of process constants of {Vi | 1 < i < n}. Now, we construct a set of rewrite rules A. The rules of types (1)-(10) are exactly the same as those of Mayr's proof and forms a defender's choice construction. (1) pT<- ->PT! (2) pT<- ^ pGr (3) pT' ' -^ pGr (4) pGr <-—> pGrV (5) pGr ±PT{ (6) pTľ ±PG1 (7) pT{< ^pGiB (8) pT{< ^pT'2 (9) pGi ^ pGiUi (10) pGi ^pT2 for all i G {1,... ,n} for all i G {1,... ,n} If there is a solution of the instance of PCP, the defender can use these rules to finish the first two rounds of the bisimulation game (starting in pTB and pT'B) in states pT2 UB and pT'2VB, where U and V form a solution of the PCP instance. The discussed first two rounds of the bisimulation game are depicted in Figure 7.4. We use the same notation for arrows as in Subsection 7.3.2. The following six rules form two subsequent rounds of the bisimulation game and allow attacker to decide whether to check equality of indices or equality of the words of U and V. In the first case, the attacker uses action b leading to the constraint check i, while the second possibility is labelled by 76 WEAK BISIMULATION EQUIVALENCE pTiB —-------vGiB pGiUB pT2UB pT'B yGiBVB pGrB------- pGrVB pT[VB si pT'2VB Figure 7.4: The first two rounds of the bisimulation game. c and ends in the constraint checko. The rewrite rules are as follows. (11) pT2 ^pT3 (12) pT'^pT* (13) pT3 —>■ check\£ (14) pT% "-^ check\£ (15) pT3 —>■ check2£ (16) pT% "-^ check2£ Now, we list the rules that serve for the checking phases mentioned in the previous paragraph. In rules (19) and (20), we use a short notation that can be easily expressed by standard rules. The rewrite rules are as follows. (17) check\Ui c— check\£ foralH G {1,. .,71} (18) check\Vic-^ check\£ foralH G {1,. .,77} (19) check2Ui ■— check2£ foralH G {1,. .,77} (20) check2Vi ■—> check2£ foralH G {1,. .,77} 7.5 CONCLUSION 77 Finally, we add rules that make the system normed. The construction of rules (21) and (22) is also discussed in Remark 30 of [May05]. The rules of type (21) enables the norm action changing the value of the store onto del. In any state, whenever the value of the store is set to del, the rules of type (22) can be used to make the state normed. Hence, A is normed in all of its states. The rules of type (23) adapt the construction to the concept of fcBPA. They make all states composed of the constraint del and a non-empty term weakly bisimilar. Tl OT'Tfl (21) ttX ^ delX for all X G Const(A) (22) delX ^ dele for all X e Const (A) (23) delX A delX for all X e Const(A) and x e Act(Ä) Hence, we have strengthen the Mayr's result [May05], Theorem 29 (also reformulated as Theorem 7.4 of this paper) as follows. Theorem 7.8. Weak bisimilarity is undecidable for normed fcBPA systems. 7.5 Conclusion First, we have shown that the weak bisimilarity problem remains undecidable for weakly extended versions of BPP (wBPP) and BPA (wBPA) process classes. We note that the result for wBPA is just our interpretation (in terms of weakly extended systems) of Mayr's proof showing that the problem is undecidable for PDA with two control states only ([May05], Theorem 29). In terms of parallel systems, our technique used for wBPP is new. To mimic the computation of a Minsky 2-counter machine, one has to be able to maintain its state information - the label of a current instruction and the values of the counters ci and C2. As a finite-state control unit of wBPP is weak, it cannot be used to store even a part of such often changing information. Hence, contrary to the constructions in more expressive systems (PN [Jan95b] and PPDA [Mol96]) we have made a term part to manage it. Further, in a test-and-decrement instruction, a process constant Lj, which represents a label of the instruction, has to be changed and one of the counters ci, C2 has to be decreased at the same time (assuming its value is positive). As two process constants cannot be rewritten by one wBPP rewrite rule, we introduce new process constants Y\ and Y2 to represent "inverse elements" to X\ and X2 respectively and we make a term X^\\Y^ to represent the counter Ck the value of which is x — y. We note that a weak finite state control unit serves for controlling the correct order of the (finitely many) successive stages in the progress of a bisimulation game. Moreover, we have shown that our undecidability results hold even for more restricted classes fcBPA and fcBPP and remain valid also for the 78 WEAK BISIMULATION EQUIVALENCE normed versions of fcBPP and fcBPA. Hence/ they hold for normed wBPP and normed wBPA as well. We recall that the decidability of weak bisimilarity is an open question for BPA and BPP. Note that these problems are conjectured to be decidable (see [May05] and [Jan03] respectively) in which case our results would establish a fine undecidability border of weak bisimilarity (see Figure 7.5). 7.5 CONCLUSION 79 undecidable decidable undecidable decidable Figure 7.5: The extended PRS-hierarchy with (un)decidability boundaries of weak bisimilarity. 80 WEAK BISIMULATION EQUIVALENCE Chapter 8 Reachability Problem In this chapter we show that the reachability problem remains decidable for the wPRS class and thus we determine the decidability borderline of the reachability problem in the extended PRS-hierarchy 8.1 Motivation A reachability problem (i.e. given two states a, ß: is the state ß reachable from the state a, written a —► * ß ?) can be considered as a basis for all model checking problems. In the beginning of Chapter 3, we indicate how a finite-state control unit (FSU) is useful for modelling of systems. On the other hand, using an FSU to extend the PRS rewriting mechanism is very powerful since the reachability problem becomes undecidable for a state extended version of PA processes (sePA) [BEH95]. Concerning decidability results, Mayr [MayOO] has shown that the reachability problem for PRS is decidable. In the context of reachability analysis one can see at least two approaches: (i) abstraction (approximate) analysis techniques on 'stronger' models such as sePA and its superclasses with undecidable reachability, e.g. see [BET03], and (ii) precise techniques for computing the set of states that are reachable from a given (regular) set of states, e.g. [LS98, EPOO, BT03]. In the latter approach, the sets are represented symbolically and various term structural equivalences are considered. The papers dealing with this approach usually work with the classes PA or PAD rather than with general PRS systems. In this chapter we study the reachability problem on the classes where the problem was open, i.e. the classes more expressive than (or incomparable with) the PRS class and less expressive than (or incomparable with) the sePA class. As the main contribution of this chapter we show that the reachability problem remains decidable for the wPRS class. This result determines the decidability borderline of the reachability problem in the ex- 82 REACHABILITY PROBLEM tended PRS-hierarchy: the problem is decidable for all classes except the sePA class and its superclasses. Moreover, the result has several interesting applications. In this chapter we mention some of them, namely • decidability of some safety properties over wPRS, • semi-decidability of weak trace non-equivalence for wPRS, and • decidability of the reachability problem for a replicative variant of Dolev and Yao's ping-pong protocols [HS05]. Some other applications can be found in the following chapters. The outline of this chapter is as follows: In Section 8.2 we show that the reachability problem is decidable for weakly extended PRS. Section 8.3 is devoted to the aforementioned applications of our decidability result. The last section summarises our results. 8.2 Reachability Problem for wPRS In this section we show that the reachability problem for wPRS is decidable. More precisely, we solve the following problem. Problem: Reachability problem for an extended (a, ß)-PRS class Instance: An extended (a, /3)-PRS system A and two of its states mt, m'ť Question: Is the state m'ť reachable from mt in A, i.e. mt —>*A m'ť ? Our proof exhibits a similar structure to the proof of decidability of the reachability problem for PRS [MayOO]. First we reduce the general reachability problem to the subproblem of reachability for wPRS with rules containing at most one occurrence of a sequential or parallel operator. Then second, we solve this subproblem using the fact that the reachability problems for both PN and PDA are decidable [May81, Buc64]. The latter part of our proof is based on our new idea of passive steps presented later. To get just a sketch of the entire proof we suggest to read the definitions and statements (skipping their technical proofs). Several of them are preceded by comments that provide some intuition. As the labels on rewrite rules are not relevant in this section, we omit them. Definition 8.1. Let Abe a zvPRS. A rewrite rule in A is parallel or sequential if it has one of the following forms: parallel rules: pX ^ q(Y\\Z) p(X\\Y) ^ qZ pX ^ qY pX ^ qe, sequential rules: pX c-^ q{Y.Z) p(X.Y) ^-> qZ pX ^-> qY pX ^-> qe, where X, Y, Z are process constants and p, q are control states. A rule is trivial 8.2 REACHABILITY PROBLEM FOR wPRS 83 if it is both parallel and sequential (i.e. it has the form pX ^-> qY or pX ^-> qe). A wPRS A is in normal form if every rewrite rule in A is either parallel or sequential. Lemma 8.2. Given a wPRS A with terms t\ and t2, we can effectively construct a wPRS A' in normal form over the same control states, along with terms t[ and t'2, such that rti —>*A SÍ2 if and only ifrt[ —>*A, st'2. Proof. In this proof we assume that the sequential composition is left-associative. It means that the term X.Y.Z is considered as (X.Y).Z, hence its proper subterms are X, Y, Z, and X.Y, but not Y.Z. However, the term Y\\Z is a subterm of X.(Y\\Z). Let size(t) denote the number of sequential and parallel operators in a term t. We put size(pt c-^ qt') = size(t) + size(ť). Given any wPRS A, let kí be the number of rules (pt c-^ qť) e A that are neither parallel nor sequential and size(ptc-^ qt') = i. Thus, A is in normal form if and only if kí = 0 for all i. In this case, let n = 0. Otherwise, let n be the largest i such that kí / 0 (n exists as the set of rules is finite). We define norm(A) to be the pair (n,kn). We now describe a procedure transforming any given wPRS A which is not in normal form and terms 11, í 2 into a wPRS A' and terms t[, t'2 such that rt\ —>*A st2 <*=>• rt[ —>*A, st'2 and norm(A') < norm(A) with respect to the lexicographical ordering on norms as pairs of integers. Let us assume that a wPRS A is not in normal form. Then there is a rule that is neither sequential nor parallel and has the maximal size. If the rule is a of the form p(Xľ.X2) ^ q{Yl\\Y2) or p(Yl\\Y2) ^ q{Xi.X2), let t be Xi.X2; otherwise, let í be a non-atomic and proper subterm of this rule. Now, replace every occurrence of the subterm t in rewrite rules of A and in the terms í 1, í2 by a fresh constant Xt. Then add two rules pXt °-> pt and pt °-> pXt for each control state p. This yields a new wPRS A' and terms t[ and t'2 where the constant Xt serves as an abbreviation for the term t. By the definition of norm we get norm(A') < norm(A). The correctness of our transformation remains to be demonstrated, namely that fh —>a si2 ^=> rt[ —>*A, st'2. The implication qV modifies a subterm t of pl\, and/or a subterm t appears in ql2 after the rule application (the other cases are trivial). If the rule modifies a subterm t of h then there are two cases. 1. Let I include the whole t. Then the corresponding rule in A' (with t replaced by Xt) can be applied directly on pl[. 84 REACHABILITY PROBLEM 2. Let I contain a part of t only. Due to the left-associativity of a sequential operator, t is not a subterm of the right part of any sequential composition in l\. Thus we apply the added rule pXt °-> pt on pl[ first and then we apply the rule in A' corresponding to the rule pi °-> qV. The situation when t appears in ql2 after the application of the considered rule is similar. Either ľ includes the whole t and then the application of the corresponding rule in A' results directly in ql'2, or t is not a subterm of the right part of any sequential composition in I2 and thus the application of the corresponding rule in A' is followed by an application of the added rule qt °-> qXt reaching the state ql'2. By repeating this procedure we finally get a wPRS A" in normal form and terms t'[,t2 satisfying rt\ —>*A st2 «=> rt" —>*A„ st2. D Mayr's proof for PRS now transforms the PRS A in normal form into a PRS A' in so-called transitive normal form satisfying (X ^-> Y) e A' whenever X —>*A, Y. This step employs the fact that rewriting under sequential rules in a parallel environment (or vice versa) has "local effect" only. Intuitively, whenever there is a rewriting sequence X\\Y —,*A (XlX^WY —+*a (XlXJWZ —+*a X2\\Z in a PRS in normal form, then the rewriting of each parallel component is independent in the sense that there are also rewriting sequences X —^*A XX.X2 —+*A X2 and Y —+*A Z. This does not hold for wPRS in normal form as the rewriting in one parallel component can influence the rewriting in other parallel components via a weak control. To get this independence back we introduce the concept of passive steps emulating the changes of a control state produced by the environment. Definition 8.3. Afinite sequence of control state pairs PS = {(pi, qi >P2 > Q2> • • • >Pn > Qnis called a sequence of passive steps, or just passive steps for short. Let Abe a zvPRS and PS be passive steps. By Aps zve denote the system A with an added rule pX ^-> qX for each (p, q) in PS and X g Const(A). Further, we define AtriV, Aseq, and Apar to be the subset of trivial, sequential, and parallel rules of A, respectively. Informally, rt\ —>*APS st2 means that the state rt\ can be rewritten into the state st2 provided a control state can be passively changed from p to q for every passive step (p, q) in PS. Please note that there is only a finite number of different sequences of passive steps for a given wPRS system. 8.2 REACHABILITY PROBLEM FOR wPRS 85 Definition 8.4. Let wPRS A be in normal form. If for every X,Y e Const(A), control states r, s, and passive steps PS it holds that rX —>*ApS sY ==> rX —>*PS sY then A is in flat normal form, triv rX —>*. pS sY ==> rX —►* PS sY then A is in sequential flat normal form, rX—>*. pS sY ==> rX—>*aPS sY then A is in parallel flat normal form. The following lemma says that it is sufficient to check reachability via sequential rules and via parallel rules in order to construct a wPRS in flat normal form. This allows us to reduce the reachability problem for wPRS to the reachability problems for wPN and wPDA, i.e. to the reachability problems for PN and PDA. Lemma 8.5. If a wPRS is in both sequential and parallel flat normal form then it is in flat normal form as well. Proof. We assume the contrary and derive a contradiction. Let A be a wPRS in sequential and parallel flat normal form. Let us choose passive steps PS and a rewriting sequence rX —>*APS sY such that rX -/->*aps sY and the triv number of applications of non-trivial rewrite rules applied in the sequence is minimal. As the wPRS A is in both sequential and parallel flat normal form, rX-/-?APS sY and rX-/-?APS sY. Hence, both sequential and parallel operators occur in the rewriting sequence rX —> *APS sY. There are two following cases. 1. Assume that a sequential operator appears first. The parallel operator is then introduced by a rule of the form pU °-> q(T\\S) applied to a state p(U.i), where í is a (possibly empty) sequential term. Note that q((T\\S).t) —>*APS sY and recall the fact that at most one process constant can be removed in one rewriting step. Hence, first of all the term T\\S is rewritten onto some single process constant V in the rest of the sequence considered. Let o be a control state after this rewriting. Using the same rewriting steps as in the original sequence, pU can be rewritten to oV in system Aps. Let PS" = PS. 2. Assume that a parallel operator appears first. The sequential operator is then introduced by a rule of the form pU <—> q(T.S) applied to a state p(U\\t), where í is a (possibly empty) parallel term. The rest of the sequence subsumes steps rewriting the term T.S onto some single process constant V. Let o be a control state in the state where T.S is rewritten to V. Contrary to the previous case, the mentioned steps can be interleaved with steps rewriting the parallel component t and possibly changing a control state. Let PS' be a sequence of control state pairs corresponding to the changes of control states caused by rewriting of the parallel component t. We merge PS' with the subsequence of PS containing only the steps employed in the considered 86 REACHABILITY PROBLEM rewriting sequence. As the result we get one sequence of passive steps denoted as PS". Please note that the elimination of the unused steps of PS ensures that PS" satisfies the definition of passive steps. Now, making use of the passive steps PS" and the steps rewriting U to V in the original sequence, we construct a rewriting sequence in system Aps leading from pU to oV. Thus we have obtained a rewriting sequence in Aps from pU to oV with fewer applications of non-trivial rewrite rules - we omit at least the first application of a non-trivial rewrite rule in the original sequence. Further, at least the first step of the new sequence is an application of a non-trivial rewrite rule. Moreover, as the number of applications of non-trivial rewrite rules used in the original sequence is minimal, we get pU —/->* Apfiv oV. This contradicts our initial assumptions about the choices of PS and the rewriting sequence in Aps. D Example 8.6. Here, we illustrate a possible change of passive steps (PS to PS") described in the second case of the proof above. Let us consider a wPRS A with control states r > p > q > t > v > o > s and the following rewrite rules rX^p(U\\Z) pU^q(T.S) v(T.S)^oV qZ ^ tY o(Y\\Y) ^ sY as well as the following sequence in Aps where PS = {(t, v)} rX ^aps p(U\\Z) —*** -^aps q((T.S)\\Z) -^aps t_((T.S)\\Y) pa^\PS passive aps v((Z&}\\Y) -^aps o(V\\Y) -^aps sY where redexes are underlined. The sequence of passive steps constructed due to the case 2 is PS" = {(q, t), (t, v)} and the constructed rewriting sequence is pU ~^aps" q(T.S) pa^eAps» t(T.S) pa^eAps» v(ZS) -^aps" oV. The following lemma employs the algorithms deciding the reachability problem for PDA and PN. Recall that the classes PDA and PN coincide with the classes of wPDA and wPN, respectively. Lemma 8.7. For every wPRS A in normal form, terms t\,t2 over Const (A), and control states r, s of A, a wPRS A' can be constructed such that A' is in flat normal form and satisfies rt\ —>*A st2 <í=> rt\ —>*A, sÍ2- Proof. To obtain A' we enrich A by trivial rewrite rules transforming the system into sequential and parallel flat normal form, which suffices thanks to Lemma 8.5. 8.3 APPLICATIONS 87 Using the algorithms deciding reachability for PDA and PN, our algorithm checks if there are some control states r, s, constants X, Y e Const (A), and passive steps PS = {(Pi, Qijj^i (satisfying r > p\ and qn > s as control states pairs out of this range are of no use here) such that rX -A* j» sY, but rX —>*PS sY or rX —>*PS sY hold. We finish ^triv ^-seq ^-par if the answer is negative. Otherwise we add to A the rules rX c—> p\Z\, qiZi ^ pi+iZi+i for í = 1,..., n - 1, and qnZn ^ sY, where Z1,...,Zn are fresh process constants; if n = 0 then we add just the rule rX ^-> sY. Hence, rX —>*\«ps sY where A" is the system A with the new rules. triv The algorithm then repeats this procedure on the system A" with one difference: the X, Y range over the constants of the original system A. This is sufficient as the new constants occur only in trivial rules. Thus, if the system with added rules is not in sequential or parallel flat normal form, then there is a counterexample with the constants X, Y of the original system A. The algorithm eventually terminates as the number of iterations is bounded by the number of pairs of states rX, sY of A, times the number of sequences of passive steps PS. The correctness follows from the fact that the added rules only duplicate existing rewrite sequences between states of A. D Theorem 8.8. The reachability problem for zvPRS is decidable. Proof. Let A be a wPRS with states rt\,st2. We want to decide whether rt\ —>*A SÍ2 or not. We assume that rt\ / SÍ2 (the other case is trivial). Clearly rt\ —>A st2 <*=>• rX —>*A„ sY, where X, Y are fresh constants and A" arises from A by the addition of the rules rX ^-> rt\ and SÍ2 °-*- sY (if t2 = e then the latter rule is not a correct rule; in this case we add to A" a rule pt °-> qY for each rule (pt °-> qe) G A instead of this incorrect rule). Lemma 8.2 and Lemma 8.7 successively reduce the question whether rX —>*A„ sY to the question whether rX —>*A, sY, where A' is in flat normal form - note that the algorithm in the proof of Lemma 8.2 does not change terms ti, Í2 if they are process constants. The definition of flat normal form implies rX —>*A, sY <í==> rX —>\, sY. Finally the triv relation rX —>\, sY is easy to check. D triv 8.3 Applications In this section we discuss some of the applications of our decidability result presented in the previous section. 8.3.1 Model Checking Some Safety Properties In the context of verification, one often formulates a property expressing that some "bad" states are not reachable. These properties are called safety 88 REACHABILITY PROBLEM properties. If the number of bad states is finite, the problem can be directly solved using reachability problem; but it is usually not the case. Usually, the bad states are characterised as those satisfying some specific property, e.g. to be a deadlock state, an internal variable x is equal to zero, stack overflows, division by zero is performed, etc. In what follows, we solve model checking for wPRS and only such safety properties that express the bad states as those where a transition with a given label is enabled. In particular, we solve a problem whether, for given wPRS A and its action bad, there is a reachable state in which a transition with the label bad is enabled. Lemma 8.9. Given a wPRS A and bad G Act(A), it is decidable whether there exists a reachable state mt such that mt -%\ nť for some state nť. Proof. The proof is done by reduction to the reachability problem. Let A = (M,<,R,mo,to). We construct a wPRS A' = (M', <', R',m0,t0), where (M', <') is (M, <) extended with a new control state r which is the least with respect to < and where R' arises from R by adding the following rewrite rules: bad . bad . (1) mil c—> rt\ for all (mt\ c—> nt2) G A, (2) rX ^ re for all X G Const (A). The rules of type (1) allow us to change any control state to r whenever a bad transition is enabled in the original system. Entering the control state r, a term can be rewritten to e using the rules of type (2). Hence, a state mt such that mt —>a nť for some state nť is reachable in A if and only if the state re is reachable in A'. D Therefore, our decidability result can be seen as a contribution to an automatic verification of infinite-state systems as well. For model checking more complex safety properties we refer to Chapter 9. 8.3.2 Semi-decidability of Weak Trace Non-equivalence Weak trace equivalence is a familiar notion which can be found already, for instance, in [Hoa80]. It is one of the semantic equivalences with a silent action r. We refer to Chapter 7 for more information about silent actions and silent moves. Here we employ a straightforward definition of weak trace equivalence, see [JEM99]. Given a labelled transition system (S, Act, —►, ao) with a distinguished action r G Act, we define the weak trace set of a state seSas wtr(s) = {w G (Act \ {t})* I s => t for some t G S}, where s ==> t means that there is some w' G Act* such that s —>* t and w is equal to w' with its r actions deleted. Two states of a system are said to 8.3 APPLICATIONS 89 be weak trace equivalent if they have the same weak trace sets. It is already known that weak trace non-equivalence is semi-decidable for Petri nets (see e.g. [Jan95a]), pushdown processes (due to [Buc64]), and PA processes (due to [LS98]). Before we strengthen the result to wPRS and all its subclasses, we prove an auxiliary lemma stating that the weak trace sets are recursive. Lemma 8.10. Given a wPRS A, its state mt, and a word w G Act(A)*, it is decidable whether w G wtr(mt) or not. Proof. We show that the problem can be reduced to the reachability problem. Let A = (M,n.,R,mo,to) be a wPRS, mt be its state, and w = w(0)w(ľ)w(2)... w(k) G (Act \ {t})+ be a word (the case w = e is trivial as mt —>*A mt). We construct a wPRS A' = (M', c', R', (m0,0), i0), where • M' = {e} U M x {0,1,..., Ä}, • C' is defined as e C' e and e C' (m, i) for all (m, i) G M', and (n, j) C' (m, í) for all (m, í), (n, j) G M' satisfying n C m and í < j, • i?' consists of the following rules: T T (1) (m, í)íi °-> (n, í)Í2 for all 0 < i < k and (mt\ c—> nt2) G A, w(i) w(i) (2) (m, í)íi °-> (n, í + 1)Í2 for all 0 < í < A; and (mt\ c-^ nÍ2j G A, w(k) w(fc) (3) (m, k)t\ "-^ ee for all (mt\ c-^ nÍ2j G A, (4) eX ^ ee for all X G čľonsŕ(A). Roughly speaking the second components of control states allow us to use the rewrite rules of type (1) labelled with r while the rules of type (2) can be used only in the order given by w. According to rules (3), the transition corresponding to the last letter of w changes the control state to e. Rules (4) then allow us to rewrite the current term to e. Hence, one can readily confirm that w G wtr(mť) with respect to A if and only if the state ee is reachable from the state (m, 0)i in the system A'. D Theorem 8.11. Weak trace non-equivalence for wPRS is semi-decidable. Proof. Let mt\ and nÍ2 be states of a wPRS A. A semi-decidability algorithm goes through all words w G (Act(A) \ {r})* and tests whether w G wtr(mt{)^wtr(nt2) orw G wtr(nt2)*\wtr(mt\). The membership of w in these sets is decidable due to the previous lemma. If the algorithm finds such a word, then two given states mt\, ní2 are weak trace non-equivalent. Moreover, if the states are weak trace non-equivalent, the algorithm will eventually find a witness w. Hence, the weak trace non-equivalence is semi-decidable. D 90 REACHABILITY PROBLEM To sum up, the border of the semi-decidability is moved up to the class of wPRS in the hierarchy. We emphasise that the semi-decidability result is new for classes PAN, PAD, and PRS of the original PRS-hierarchy, too. As the reachability problem is undecidable for the other classes of the extended PRS-hierarchy (i.e. sePA and its superclasses), it is easy to see that the weak trace non-equivalence is not even semi-decidable for them. 8.3.3 Other Applications The decidability of the reachability problem for wPRS has recently been applied in the area of cryptographic protocols. Hüttel and Srba [HS05] define a replicative variant of a calculus for Dolev and Yao's ping-pong protocols [DY83]. They show that the reachability problem for their calculus is decidable as it can be reduced to the reachability problem for wPRS. We note that this application does not employ the full power of our result, as all the systems produced by the reduction mentioned belong to wPAD class. 8.4 Conclusion We have shown that an extension of the Process Rewrite System mechanism with a weak finite-state control unit (wPRS) keeps the reachability problem decidable. Some applications of this result have been discussed as well, namely those of model checking some safety properties and semi-decidability of weak trace non-equivalence for wPRS. We also noted that the decidability of the reachability problem for wPRS has already been used in [HS05] to show that the reachability problem for a replicative variant of a calculus for Dolev and Yao's ping-pong protocols is decidable. 8.4 CONCLUSION 91 sePRS undecidable decidable nAri s^ wPAD sePAN undecidable decidable wPAN Figure 8.1: The extended PRS-hierarchy with (un)decidability boundaries of the reachability problem. 92 REACHABILITY PROBLEM Chapter 9 Branching Time Logics In this chapter we examine the problem whether a given weakly extended process rewrite system (wPRS) contains a reachable state satisfying a given formula of Hennessy-Milner logic. We show that this problem is decidable. As a corollary we observe that also the problem of strong bisimilarity between wPRS and finite-state systems is decidable. Decidability of the same problem for wPRS subclasses, namely PAN and PRS, has been formulated as an open question, see e.g. [Srb02a]. We also strengthen some related undecidability results on some PRS subclasses. 9.1 Motivation Research on the expressive power of process classes has been accompanied by exploring algorithmic boundaries of various verification problems. In this chapter we focus on model checking some (fragments of) simple branching time logics, namely EF and EG. Most of verification problems studied here are known as reachability properties. Such properties express that some some "bad" state(s), for example deadlock, should not be reached along any execution path or that some "good" state(s) should be reached along at least one execution path. The former can be naturally expressed as —lEFcp where a formula if characterises the set of states which should not be reached, while the latter can be stated as EEip where if characterises the set of states to be reached. Now, we briefly recall the state of the art for EF and EG logics on PRS subclasses; details can be found in [BCMS01] and references given there. Also we mention our contribution using wPRS and sePRS subclasses. First, we recall that the reachability problem, i.e. to decide whether a given state is reachable from the initial one, is decidable for the classes of PRS [MayOO] and wPRS (Theorem 8.8), while it is undecidable for sePA [BEH95]. See Chapter 8 for more information. All the problems mentioned below remain undecidable on the sePA class due to its Turing power. 94 BRANCHING TIME LOGICS A reachability property problem, for a given system A and a given formula if, is to decide whether EFip holds in the initial state of A. Hence, these problems are parametrised by the class to which the system A belongs, and by the type of the formula if. In most of practical situations, if specifies error states and the reachability property problem is a formalisa-tion of a natural verification problem whether some error state is reachable in a given system. We recall that the (full) EF logic is decidable for the PAD class, as shown in [May98]. It is undecidable for PN [Esp94]; an inspection of the proof moves this undecidability border down to PPDA. If we consider the reachability HM property problem, i.e. the reachability property problem where

c ol A (a!, C) |=

*c a' A (a',£)\=

1 We write L\= tpiftp is valid in the initial state cto of L. Definition 9.3. For each UB formula

, we define depth(ty) as a nesting depth of (a) operators in

by induction on the structure of the formula: depth(tt) = 0 depth(^ip) = depth((p) depth((p Aip) = mdJi{ depth (ip), depth(ip)} depth((a)(p) = depth((p) + 1 depth(EEip) = depth((p) depth(EG(p) = depth((p) Introducing some restriction on the syntax level, we define four fragments of UB logic. • A UB formula

• A UB formula p is called a simple formula if it is an HM formula satisfying depth(p) = 1. Hence, the syntax of simple logic is defined as (/? ::= tt \ -tip \ p, i.e. L(A) \= EGp ? 9.3 REACHABILITY HM PROPERTY 97 Problem: Evitability simple property for C Instance: A simple formula if and a system A e C Question: Is the system A a model of a formula EGip, i.e. L(A) \= EGip ? It is easy to see that the reachability simple property problem is a sub-problem of the reachability HM property problem, that is, again, a sub-problem of the decidability of EF logic. The same holds for the three EG properties given above. Other combinations are incomparable. The situation can be depicted as follows. decidability EF logic reachability HM property reachability simple property decidability EG logic evitability HM property evitability simple property 9.3 Reachability HM Property In this section, we study a reachability HM property problem for wPRS, i.e. the problem to decide whether a given wPRS A and a given HM formula if satisfy A |= EEip or not. We prove that the problem is decidable. The proof reduces this problem to the reachability problem for wPRS, i.e. the problem to decide whether a given state of a given wPRS is reachable or not, which is decidable due to Theorem 8.8. For the rest of this section, let A be a fixed wPRS system, D g" Const(A) be a fixed fresh process constant, and C = Const (A) U {D}. Further, let if be a HM formula and n = depth(ip). We assume that n > 0. Definition 9.4. A term ť is called n-equivalent to a state pt of A if and only if for each HM formula tp satisfying depth(tp) < n, it holds: (A,pt)\=ip {A,pt')\=4> Our proof will proceed in two steps. In the first step we show that there exists afinite set T of terms such that, for each reachable state pt of A, the set T contains a term ť which is n-equivalent to pt. In the second step we enrich the system with rules allowing us to rewrite an arbitrary reachable state pt to a state [p, ť] D, where the control state [p, ť] represents the original control state p and a term ť which is n-equivalent to pt. Finally, for each p G M(A),ť G T satisfying (A,pť) \= f we add a rule [p, ť] D A acc D. Let us note that the validity of (A,pť) \= (p is decidable as wPRS systems are finitely branching. To sum up, if is valid for some reachable state pt of A if and only if the state acc D is reachable in the modified system. 98 BRANCHING TIME LOGICS First, we introduce some auxiliary terminology and notation. A nonempty proper subterm ť of a term t is called idle if ť is the right-hand-side component of some sequential composition in t (such that its left-hand-side component is nonempty), where sequential composition is considered to be left-associative. For example, a term (X.Y.Z)||(č7.(V||ľ4A)) should be interpreted as {{X.Y).Z)\\{U.{V\\W)) and its idle subterms are Y, Z, V\\W but not Y.Z. By IdleTerms we denote a set of all idle terms occurring in the initial term or in terms on the right-hand sides of rewrite rules of A. Observe that each idle subterm of any reachable state of A is contained in IdleTerms. We define a length of a term t, written |i|, as the number of all occurrences of process constants in the term. For example, |X||(X.F)||e| = 3. Formally, length of a term is defined by induction on the term structure as follows. \e\ =0 \X\ = 1 M2| = |ii| + M |íl||Í2| = |íl| + N Further, for each j > 0, we define a set SmallTerms(j) = {t \ t is a term over C and 0 < |i| < j}. Definition 9.5. Let h > 0 be an integer. We put k = max{|i| | t G IdleTerms} and H = h ■ (h + k) ■ \SmallTerms(h + k)\. We define Rules(h) to be the set of rewrite rules of three types (see the proof of Lemma 9.6 for their respective roles): del (1) p (s'.D) ^ pD for all p G M (A) and s1 G SmallTerms(H), (2) psh+l "-^ psh f or all p G M (A) and s G SmallTerms(H), del (3) p (s'.s) "-^ pD for all p G M (A), s G IdleTerms, and s' G SmallTerms(H) \ SmallTerms(h), where s% denotes a parallel composition of i copies of term s. Lemma 9.6. Tor each h > 0 and for each reachable state pt of A it holds that P(t.D)^*Rules(h)pD. Proof. As every rule in Rules(h) has its right-hand side shorter than its left-hand side and an application of a rule in Rules(h) cannot produce any new idle subterm, it is sufficient to prove that, for each p G M(A) and each term t over C with all idle subterms in IdleTerms, there is a rule of Rules(h) applicable to p (t.D). We assume the contrary and derive a contradiction. Let p G M (A) be a control state and í be a term of the minimal length such that t satisfies the preconditions and no rule of Rules(h) is applicable to p (t.D). Then |í| > H as in the other case a rule of type (1) is applicable to p (t.D). There are two cases: 9.3 REACHABILITY HM PROPERTY 99 t = u.v As v G IdleTerms we have |t>| < k. Further, |í| > H implies \u\ > H — k > h. If h < \u\ < H, then there is a rule of type (3) that can be applied to p (t.D). Hence \u\ > H. As no rule of Rules(h) can be applied to p (t.D) = p (u.v.D), no such rule can be applied to pu. The inequality \u\ > H gives us that a rule of type (1) is applicable to p (u.D) if and only if it is applicable to pu. The same holds for rules of type (2) and (3) as well due to the shape of these rules and due to the fact that D does not occur in any term of IdleTerms. To sum up, no rule of Rules(h) can be applied to p (u.D) and thus u contradicts the minimality of t. t = u\\v As '|ľ is associative and commutative, it can be seen as an operator with an unbounded arity Thus, t can be seen as a parallel composition of several components which are nonempty sequential terms. The length of each of these components is less than or equal to H; a component u satisfying \u\ > H would contradict the minimality of t using the same arguments as in the previous case. Further, as no rule of type (3) can be applied, the length of each component is at most h + k. Moreover, as rules of type (2) are not applicable, we have that the parallel composition contains at most h copies of each component. Hence, |i| < h ■ (h + k) ■ \SmallTerms(h + k)\ = H. This contradicts the relation |i| > H. D Definition 9.7. Let I be the maximal length of a left-hand-side term of a rule in A. Lemma 9.6 implies that, for each reachable state pt of A, there exists a transition sequence pit.D) —¥*RUies(ni) P-D- % MultiSetni(pt) (or just MultiSet(pt) if no confusion can arise) we denote a multiset containing exactly all the subterms that are rewritten during this transition sequence and correspond to a subterm s' of rewrite rules of types (1) and (3). Further, for each multiset of terms S = {či,Č2, • • • ,tj}, we define its characteristic term ts = (h.D)\\(t2.D)\\...\\(t3.D). Lemma 9.8. Let pt be a reachable state of A. Then tMuiuset(pt) *'s n-equivalent to pt. Proof. Let us fix a transition sequence p (t.D) —v*RUies(ni) P^ anc* the corresponding multiset MultiSet(pt). The proof proceeds by induction on the number of transition steps in the transition sequence. Let Si denote a part of MultiSet(pt) obtained in the first i transition steps and pui be the state reached by these steps. It is sufficient to prove that, for each i, Ui\\tst is n-equivalent to pt. We note that D cannot be rewritten by any rewrite rule of A - it is used to prevent unwanted rewriting. The basic step is trivial as uq = t, So = 0, and thus Ui \\tsi =t\\e. Now we assume that «iHi^ is n-equivalent to pt and we prove that the same holds 100 BRANCHING TIME LOGICS for Ui+\ \\tsi+1- Let I be the maximal length of a left-hand-side term of a rule in A. There are three cases reflecting the type of the rewrite rule applied in a transition step pui -^Ruies(ni) pui+i: type (1) We note that no rule in Rules (nl) can introduce D on the right- del hand side of a sequential composition. Thus, a rule p(s'.D) °-> pD of type (1) is applicable to pui iff Ui = s'.D. Therefore, Ui+\ = D, St+i = StU{s'},andut+i\\tSitl = D\\(s'.D)\\tSi = D\\ut\\tSi. Asut\\tSi is n-equivalent to pt, it is obvious that so is Ui+i\\tsi+1. type (2) Let ip be an HM formula such that depth(ip) < n. Then its validity in a state depends only on the first n successive transitions per-formable from the state. At most nl process constants of the term t can be rewritten during n successive steps. Hence, at most nl parallel components can be rewritten during these steps. Thus, reducing of the number of identical parallel components from nl + 1 to nl does not affect the validity of ip. To sum up, Ui+i\\tsi+1 = «j+iHi^ is n-equivalent to pt. type (3) The term s' occurring in the applied rule satisfies \s'\ > nl. Hence, the part of the term t corresponding to the subterm s of the rule is "too far" to be rewritten in the first n steps of any transition sequence. The term s'.s in Ui is replaced by D in Ui+\. It is easy to see that Ui+i\\tSi+1 = ui+i\\(s'.D)\\tSi is n-equivalent to pt. D Given a multiset of terms S, by S[n we denote the largest subset of S containing at most n copies of each element. One can readily confirm that a characteristic term ts is n-equivalent to some state of A if and only if t s in is n-equivalent to this state. To sum up, for each reachable state pt of A, we can construct a multiset MultiSet(pt)in such that its characteristic term tMultiSet(pt^n is n-equivalent to pt. Moreover, there is a bound on the size of each such a multiset which depends on A and n only. More precisely, such a multiset contains at most n copies of terms s' G SmallTerms(nl ■ (nl + k) ■ \SmallTerms(nl + k)\), where I is the maximal length of a left-hand-side term of a rule in A and k is the maximal length of a term in Idle Terms. We now present the reduction of the reachability HM property problem for wPRS to the reachability problem for wPRS. Lemma 9.9. Let A be a wPRS system and ipbea Hennessy-Milnerformula. Then we can construct a zvPRS A' with a state ace D such that A |= EFíp <í==> ace D is reachable in A'. 9.4 COROLLARIES AND REMARKS 101 Proof. Let n, D, C, IdleTerms, SmallTerms(j), and MultiSet(pt) have the same meanings as above. Let k be the maximal length of a term in IdleTerms, I be the maximal length of a left-hand-side term in any rule from A, and H = nl ■ (nl + k) ■ \SmallTerms(nl + k)\. Further, let S be a set of all multisets containing at most n copies of each term s' G SmallTerms(H). The system A' uses control states of the original system, a distinguished control state ace G" M (A), and control states of the form (p, S) where p G M(A) and S G S. Let poh be the initial state of A. Then A' has the initial state po (to-D) and the following rules, where p and S range over M(A) and S respectively. We omit labels as they are not relevant. (1) pt ^ qť for all (pt A qť) G A (2) pX ^ (p, 0) X for all X G C (3) [p, S) s'.D ^ (p, (S U {s'})in) D for all s' G SmallTerms(H) (4) (p, S) snl+l ^ {p, S) snl for all s G SmallTerms(H) (5) (p,S)s'.s^(p,(Su{s'})in)D for all s G IdleTerms and s' G SmallTerms(H) \ SmallTerms(nl) (6) (p, S) D c^r acc D whenever (A, pts) |= <ŕ> Intuitively, the rules of type (1) mimic the behaviour of A and enable A' to reach a state p (t.D) if and only if pt is a reachable state of A. A rule of type (2) stops this mimic phase and starts a checking phase where only rules of types (3)-(6) are applicable. The rules of types (3), (4), and (5) correspond to the rules of type (1), (2), and (3) in Rules(nl), respectively. Let p (t.D) be a final state reached in the mimic phase. The rules of types (3)-(5) allow us to rewrite this state to the state (p, MultiSet(pť)[n) D. Finally, the control state (p, MultiSet(pt)[n) can be changed to acc using a rule of type (6) if and only if (A, tMvUiSet{pt)in) |= Z, 7 Intuitively, the construction enriches a given PRS with and additional rules enabling folding and unfolding of large terms. The construction of [May98] also introduces 7 rules to sign intermediate states during folding and unfolding. The problem is that neither the a action nor the 7 action is enabled in the state with the unfolded term. We do not see any easy way how to repair the construction. For example, labelling the folding rules by 7 does not help because it cause other problems (e.g. folding part of one rewriting action can disturb performing of other action). 9.5 EVITABILITY SIMPLE PROPERTY FOR DETERMINISTIC BPP_________103 Remark 9.14. It is known that (full) EF logic is undecidable f or PN [Esp94]. An inspection of the proof given in [Esp97] shows that this undecidability result is valid even for seBPP class. 9.5 Evitability Simple Property for Deterministic BPP Esparza and Kiehn have proved that EG logic is undecidable for (deterministic) BPP [EK95]. In this section we describe a modification of their proof showing that for (deterministic) BPP even the evitability simple property problem is undecidable. As we just describe the necessary changes to be done within the proof given in [EK95], we use the same notation as introduced in their paper. The original proof is done by a reduction from the halting problem of a Minsky counter machine. A quick inspection of the reduction shows that it demonstrates undecidability of the inevitability HM property problem for the class of deterministic BPP systems. We note that it is not a proof of undecidability for the inevitability simple property problem due to the following reason. In the definition of EN(a\,..., au), there is a subformula k k A -<3(aí)EN(aí) corresponding to K^{di){di)tt in our notation i:=\ i=\ which expresses that no sequence uíuí is enabled. Omitting this subformula from EN(a\,..., a^), the construction produces a simple property formula. In what follows, we present some other changes to be done within the construction in order to keep its correctness for the case of the simple property formula as well. In other words, we prove that even the inevitability simple property problem remains undecidable for the deterministic BPP systems. The following definitions of SM, M, and C j are the same as in [EK95]: SMd= (SQiH ... ||SQn+i) Md=fSM||Qo Cj d= dec] • dec^ • dec^ • 0 Without loss of generality, we assume that there is no self loop in the counter machine M (i.e. k / i / k', for each transition rule of M). Hence, it is not necessary to create a new parallel instance of a process constant Q± from SQi as far as the rewriting on the existing instance of Q± is not finished. In the following, we reformulate the definitions of SQi and Qi to prevent sequences of the form out{out{ or out?out?. The halting state definition is reformulated as follows. del .1 del SQn+i = mn+1 ' Qn+i Qn+i = halt • SQn+1 104 BRANCHING TIME LOGICS A state Qi of type II is modelled as follows. „„ def . i _ _ def i o __ SQi = inj; • Qi Qi = out j • ouq • SQi A state qi of type I has to proceed to the state qt- To prevent multiple occurrences of the process constant Qk, we use the same technique as in the case of states of type II. Hence, SQi and Qi are modelled as «« def i „ „ def i o ,„„ n« \ SQi = inj • Qi Qi = outj • oirq • (SQi||Cj) and we add the following disjunct to the formula EN(dec]) A -.£iV(a, if there is no transition pt —a. p'ť for any state p'ť and any action a. In this chapter we consider only systems where the initial term is a single constant (see Remark 2.9). Moreover, we always consider only systems where the initial state is not terminal. This restriction do not cause any weakening of our results. It is easy to determine that the initial state is terminal and deciding model checking problem is easy for this case, too. Definition 10.1. A (finite or infinite) sequence «1 «2 a„ ( ÍJn+l \ G = p\t\ -----A. P2l2 -----A. • • • -----A. Pn+ltn+1 ( ----->A • • • I is called a derivation over the word u = aici2 ■ ■ ■ an(an+i...) in A. A derivation in A is called a run of A if it starts in the initial state poX0 and it is either infinite, or its last state is terminal. Finite derivations are also denoted as piti —>*A pn+itn+i, infinite ones as piii —>A . Further, L (A) denotes the set of words u such that there is a run of A over u. Definition 10.2. For technical reasons, we define a normal form ofwPRS systems. A rewrite rule is parallel or sequential if it has one of the following forms4} ^ote that, due to technical reasons, the parallel rules of this definition are not as restrictive as those of Definition 8.1. 112 LINEAR TIME LOGIC Parallel rules: p(Xi\\X2\\... \\Xn) c—> q(Yi\\Y2\\... \\Ym) Sequential rules: pX ^-> qY.Z pX.Y ^-> qZ pX ^-> qY pX ^-> qe where X,Y,Xi,Yj,Z G Const, p, q G M, n > 0, m > 0, and a G Act. A rule is called trivial if it is both parallel and sequential (i.e. it has the form pX ^-> qY or pX ^ qe). A wPRS A is in normal form if it has only parallel and sequential rewrite rules. Linear Temporal Logic The Linear Temporal Logic (LTL) [Pnu77] can be (equivalently) defined with use of various sets of temporal operators. In the following definition, we employ just two common future temporal operators, namely next and until, and two common past temporal operators, namely previously and since. Definition 10.3. Let Act = {a, b, ■ ■ ■ } be a countably infinite set of atomic actions. The syntax of Linear Temporal Logic (LTL) is defined as ip ::= tt | a \ -itp \ ip A if \ Xtp \ if U Lp \ Yip \ , and <^ are derived operators defined in the very standard way. Later on, we also define other modalities as abbreviations of expressions based on the defined four modalities. The logic is interpreted over infinite as well as nonempty finite words of actions. Given a word u, by \u\ we denote the length of u (for infinite words we put \u\ = oo). An empty word e has a zero length. A concatenation of a finite word v and a word u is denoted by v.u or vu. For all 0 < i < \u\ by u(i) we denote the (i+l)th letter of u, i.e. u = u(0)u(l)u(2)... u(\u\ — 1) if u is finite and u = u(0)u(l)u(2)... otherwise. Further, for all 0 < i < \u\ by Ui we denote the ith suffix of u, i.e. Ui = u(i)u(i + l)u(i + 2)... u(\u\ — 1) if u is finite and Ui = u(i)u(i + l)u(i + 2)... otherwise. A pointed word is a pair (u, i) of a nonempty word u and a position 0 < i < \u\ in this word. The semantics of LTL formulae is defined inductively in the following definition. Definition 10.4. Let Lp he an LTL formula and (u, i) he a pointed word. We define that a formula

is valid for the position í in the word u, written (u, i) \= Lp, by induction on the structure ofu. 10.2 DEFINITIONS OF THE STUDIED PROBLEMS 113 (u,i) (u,i) (u,i) (u,i) (u,i) (u,i) (u,i) (u,i) \=tt |= a iff u{i) = a 1= -V iff (u, i)¥=

(u,i) |=^i)) |= Y<£ iff 0 (u,i) |=^i)) We say that a nonempty word u satisfies Lp, written u |= Lp, if and only if (u, 0) |= (/?. Given a set of words L, we write L \= Lp if u \= Lp holds for all u G L. We say that a derivation (or run) a over a word u satisfies Lp, written a |= Lp, whenever u\= tp. Considering all pointed words or just the pointed words of the form (u, 0) yields different notions of equivalence. Definition 10.5. Let Lp and tp be LTL formulae. The formulae are said to be (initially) equivalent, written Lp =j tp, if for all words u we have u |= Lp if and only if u \= tp. The formulae are said to be globally equivalent, written Lp =g tp, if for all words u and for all positions 0 < í < \u\ we have (u, i) |= Lp if and only if (u, i) \= tp. One can readily confirm that if two formulae are globally equivalent then they are also initially equivalent. Remark 10.6. Let us mention that there is no difference between initial and global versions of equivalence as far as we consider only so called future modalities like until and next. Indeed, for all pointed words (u, i) and all formulae Lp containing these future modalities only, it holds that (u, i) |= Lp if and only if Ui \= Lp and hence the initial and global equivalences coincide. Contrary, the difference between initial and global versions arises as soon as past modalities are introduced. 114 LINEAR TIME LOGIC modality meaning name X U see Definition 10.4 see Definition 10.4 next until F G FIP =g ttUtf G(f =g -lF-lt£> eventually always Fs Gs Fs<£ =g XFtp Gstp =g _,Fs-i^ strict eventually strict always oo F oo G oo Ftp =g GFtp OO OO Qtp =g -^F^tp infinitely often almost always Y S see Definition 10.4 see Definition 10.4 previously since P H Ptp =g ttStp F\tp =g -iP-llfi eventually in the past always in the past Ps Hs PS^ =g YP^? F\Stp =g -^PS^tp eventually in the strict past always in the strict past 1 \IP =g F\P^ initially Figure 10.1: LTL modalities overview In Figure 10.1 we enrich the syntax of LTL with other modalities. For the sake of completeness, the presented list of modalities includes also the operators which has been already defined. Note that Ftp is equivalent to tp v Fstp but Fstp cannot be expressed with F as the only modality. Thus Fs is "stronger" than F. The same relations hold between Gs and G, Ps and P, and Hs and H. For a set {0\,..., On} of modalities, let LTL(Oi,..., On) denote the LTL fragment containing all formulae with modalities 0\,..., On only. Such a fragment is called basic. Figure 10.2 shows an expressiveness hierarchy of all the basic LTL fragments studied here. Indeed, every basic LTL fragment using standard2 modalities is (initially) equivalent to one of the fragments in the hierarchy. For example, any LTL(S, Y) formula is initially equivalent to a formula without any modality. Hence, every LTL(U, X, S, Y) formula tp can be effectively translated into a formula of LTL(U, X) that is 2By standard modalities we mean the ones defined here and also other commonly used modalities like strict until, release, weak until, etc. However, it is well possible that one can define a new modality such that there is a basic fragment not equivalent to any of the fragments in the hierarchy. 10.2 DEFINITIONS OF THE STUDIED PROBLEMS 115 initially equivalent. To sum up, every LTL formula with arbitrary modalities is initially equivalent to a formula of LTL(U, X). Let us also note that, e.g. LTL(FS) = LTL(FS, Gs) even with respect to global equivalence. Further, the hierarchy of Figure 10.2 is strict with respect to initial equivalence. For detailed information about expressiveness of LTL modalities and LTL fragments we refer to [Str04]. Model Checking Problem Let T be an LTL fragment and C be a class of systems. Problem: Model checking problem for T and C Instance: A formula if e T and a system A e C Question: Is the system A a model of the formula if, i.e. L (A) \= 0, • 0i G LTLQ for each í < n + 1, • O i is either V or V+' or 'A X' for each í < n, and • On is 'A Gs'. Further, let B c LTL Q be afinite set. An a-formula is defined as a(s,B) = {e1o1(e2o2■ ■ ■ (enonen+1)...)) a f\ gsfs^ The A fragment consists of finite disjunctions of a-formulae. Hence, a word u satisfies a (6, B) if and only if u can be written as UI.U2---- .Un+1 where • each Ui, for i = 1,... ,n + l, consists only of actions satisfying 9 í and - \ui\ > 0 if i = n + 1 or Oi is 'U', - \ui\ > Oif Oi is'U+', - \uiI = 1 if Oi is 'A X' or 'A Gs', and • un+\ satisfies GSFS^ for every ip G B. Lemma 10.9. A conjunction of a-fortnulae can be effectively converted into an equivalent disjunction of a-fortnulae. Proof of this lemma is a simple but very technical exercise and we sketch only the basic ideas here. 118 LINEAR TIME LOGIC Proof (sketch). Let a(ö\, B\) and a(Ö2, #2) be the two disjuncts. Clearly, the set B of each a-formula of the desired disjunction is £>i U £>2. Each ö part (see Definition 10.8) of an a-formula can be represented as a weak finite state automaton3 accepting exactly those words that models the ö formula.4 Vice versa, every weak automaton can be represented as a disjunction of ö formulae. In particular, every ö formula stays for one "loop-less" run from the initial state to an accepting state. Therefore, we construct a synchronous product of two weak automata representing či and 62- It is clear that the resulting automaton is also weak. Hence, there is a disjunction of ö formulae representing the automaton. These ö formulae compose the required disjunction of a-formulae. D Theorem 10.10. Every LTL(FS, Gs) formula can be translated into an equivalent disjunction of a-formulae. Proof. As Fs and Gs are dual modalities, we can assume that every LTL(FS, Gs) formula contains negations only in front of actions. Given an LTL(FS, Gs) formula if, we construct a finite set Av of a-formulae such that

) = (Fsa) A (GsFs(/>), we set Av = {a(tt U+ Ö, B) \ a(ô, B) e A^}. •Gs Case Gs(^i: This case is divided into the following subcases according to the structure of 3 A ^4): This case is also divided into subcases depending on the formulae if 3 and if 4. *p Case GsFs(p3 A ^4): As p3 A p4 G LTL(), this subcase has already been covered by Case GsFsp. *V Case GSFSQ?3 A (ip5 V ipe))- As GSFS(^3 A (ip5 V ipe)) = GSFS((^3 A 5), the set Av can be constructed from AqspsIP3 and ^gsfs 3: A word u satisfies GSFSGS(£>3 iff \u\ = 1 or u is an infinite word satisfying FSGS(£>3. Note that Gs—iřř is satisfied only by finite words of length one. Further, a word u satisfies (Fsřř) A (GsFsŕŕ) iff u is infinite. Thus, GSFSGS(£>3 = (Gs--řř) V 2 V hfi)'- It holds that Gs(t£>2 V hfi) = (Gs^2) V Fs(Fst£>4 A Gstf2) V GsFs(/?4. Therefore, the set Av can be constructed as AqsV2 U {a(tt(J+ö,B) \ a(ö,B) G ApsV4AQsV2} U 120 LINEAR TIME LOGIC AgsfsV>4, where AFsip4AGsip2 is created from AFsip4 and AGsip2 due to Lemma 10.9. *GS Case Gs(ip2 V Gsip4): There are only the following two subcases (the others fit to some of the previous cases). (Í) Case Gs(V^eG Gs¥/): It holds that Gs(V^eG GsV') = (Gs-ttfyvSJ ,eG(XGs}. (ii) Case Gs(p2 V V^ec W): As Gs(p2 V V^ec G^0 = (Gsp2) V V¥,'ec(x(P2 U Gst//)). Therefore, the set A^, can be constructed as AqsP2 U U^'ggÍ^C^ a ^P? U č, £>) \ a(ô,B) G AGsip,}. oGs Case GsGst£>2: As GS(GS<£2) = (Gs-tfr) V (XGS^2), the set A^, can be constructed as AQs-,tt U {a(řř A Xö, B) \ a(ö, B) G AqsIP2 }. D 10.4 Model Checking of wPRS against Negated A This section is devoted to decidability of the model checking problem for the wPRS class and negated formulae of the A fragment. In fact, we prove decidability of the dual problem, i.e. whether a given wPRS system has a run satisfying a given formula of A. Finite and infinite runs are treated separately. Theorem 10.11. The problem whether a given wPRS system has afinite run satisfying a given a-formula is decidable. Proof Let A be a wPRS system and a(ö, B) be an a-formula. Note that a formula GSFS^ is valid on a finite nonempty word if and only if the length of the word is 1. Therefore, if B / 0 then it is easy to check whether there is a finite run of A satisfying a(ö, B). In what follows we assume B = 0. Let ö = Q101Q202 • • • 9nOn9n+i. We construct a wPRS system A' with control states M (A) x{l,2,...,n + l}in the following way. • For any 1 < i < n and every rule pt\ c-^ qt2 of A such that a satisfies 6i, we add to A' the rule (p, i)t\ c-^ (q,i + l)t2 and if 0% is U or U+ then also the rule (p, í)t\ ^-> (q, i)t2. • For every p G M (A), X G Const (A), and for any 1 < i < n such that Oi = U, we add to A' the rule (p, i)X °-> (p, i + 1)X, where e is an arbitrary action. • For every rule pt\ c-^ qt2 of A such that a satisfies 9n+\, we add to A' the rule (p, n + l)ii ^-> (q, n + l)t2. 10.4 MODEL CHECKING OF wPRS AGAINST NEGATED A 111 • For every rule pt\ °-> qt2 of A we add to A' the rule (p, n + l)ii °-> {p,n + l)ti. Let pqXq be the initial state of A. There is a finite run pqXq —>*A qt satisfying a(ö, 0) if and only if there is a finite run (po, 1)Xq —>*A, (q,n + l)i. Hence, we need to decide whether there exists a state of the form (q,n + l)t that is terminal and reachable from (po,l)Xo. To do that, for every p G M (A) we add to A' the rule (p,n + l)Z ^-> (p, n + l)e, where end G" Act(A) is a fresh action and Z G" Const (A) is a fresh process constant. Now, it holds that A has a finite run satisfying a (6,0) if and only if there exists a state of A', which is reachable from (po, l)(Xo\\Z) and the only enabled action in this state is end. This last condition on the state can be expressed by formula if = (end)tt A A«eAcí(A) ^{a)H of the Hennessy-Milner logic. As reachability of a state satisfying a given Hennessy-Milner formula is decidable for wPRS (see Chapter 9 for details), we are done. D The problem for infinite runs is more complicated. In order to solve it, we introduce more terminology and notation. First we define ß-formulae and regular languages called ^-languages. Let w = a\ö\a2Ö2 ■ ■ ■ anOn, where n > 0, a\,..., an G Act are pairwise distinct actions and each Oi is either 'U+' or 'AX'. Further, let B C Act \ {a\,..., an} be a nonempty finite set of actions and C C B. A /3-formula ß(w, B, C) and 7-language 7(10, C) are defined as ß(w, B, C) = (aiOi(a202 ... (anOnG \J b)...)) A /\ GF6 A /\ (Ffe A --GF&) beB bec beB-^c j(w,C) = al1 .a°22. ■ ■ ■ .a°nn.L, + if 0% = U+ = í {e} if C = 0 1 ifOí = AX an j f]beCC*.b.C* otherwise Roughly speaking, a /3-formula is a more restrictive version of an a-formula and in context of /3-formulae we consider infinite words only. Contrary to ö of an a-formula, w of a /3-formula employs actions rather than LTLQ formulae. While a tail of an infinite word satisfying an a-formula is specified by 9n+\, in the definition of /3-formulae we use a set B containing exactly all the actions of the tail and its subset C of exactly all actions occurring infinitely many times in the tail. Remark 10.12. Note that an infinite word satisfies a formula ß(w, B, C) if and only if it can be divided into a prefix u G 7(10, B) and a suffix »eC" such that v contains infinitely many occurrences of every c G C. Let w,B,C be defined as above. We say that a finite derivation a over a word u satisfies 7(10, C) if and only if u G 7(10, C). We write («/, B1) n. where o% = 122 LINEAR TIME LOGIC (w, B) whenever B' C B and w' = a^O^a^O^ ... dikOik for some 1 < i\ < Í2 < ... < ik < n. Moreover, we write («/, B', C') C (w, B, C) whenever (V, B') n (w, B), B' is nonempty, and C" C C n B'. Remark 10.13. If u is an infinite word satisfying ß(w, B, C) and v is an infinite subword of u (i.e. it arises from u by omitting some letters), then there is exactly one triple («/, B', C) c (w, B, C) such that v \= ß(w', B', C). Further, for each finite subword v of u, there is exactly one pair («/, B') such that («/, B') c (w,B) andv G j(w',B'). Given a PRS in normal form, by tri (A), par (A), and seq(A) we denote the system A restricted to trivial, parallel, and sequential rules, respectively. A derivation in tri(A) is called a trivial derivation in A. In the following we write simply tri, par, seq as A is always clearly determined by the context. Definition 10.14. Let A be a PRS in normal form and ß(w, B, C) be a ß-formula. The PRS A is in flat (w, B, C)-form if and only if for each X,Y e Const(A), each («/, B', C) c (w, B, C), and each B" c B, the following conditions hold: 1. If there is afinite derivation X -^* Y satisfying j(w', B"), then there is also afinite derivation X —>*tri Y satisfying j(w', B"). 2. If there is a term t and a finite derivation X -^* t satisfying j(w', B"), then there is also a process constant Z and afinite derivation X —>*tri Z satisfying j(w', B"). 3. If w' = e and there is an infinite derivation X -^ w satisfying ß(w', B', C), then there is also an infinite derivation X —>%ri satisfying ß(w',B',C). 4. If there is an infinite derivation X —>^ar satisfying ß(w',B',C'), then there is also an infinite derivation X —>%ri satisfying ß(w', B', C"); 5. If there is an infinite derivation X -^^eq satisfying ß(w',B',C'), then there is also an infinite derivation X -—^ri satisfying ß(w', B', C'). Roughly speaking, a system is in flat (w,B, C)-form if for every derivation of the form given in the definition there is an "equivalent" trivial derivation. Proposition 10.15 (Fairness problem [Boz05]). For X,Y G Const(A) and K, K u c Act (A) it is decidable whether there is an infinite derivation of the form X -^ such that all actions of K occur in u and all actions of K^ occur infinitely many times in u. 10.4 MODEL CHECKING OF wPRS AGAINST NEGATED A 123 All conditions of the Definition 10.14 can be checked due to the following lemma, Proposition 10.15 , and decidability of LTL model checking for PDA and PN. Lemma 10.17 says that every PRS in normal form can be transformed into an "equivalent" flat system. Finally, Lemma 10.20 says that if a PRS system in flat (w,B, C)-form has an infinite derivation satisfying ß(w, B, C), then it has also a trivial infinite derivation satisfying ß(w, B, C). Note that it is easy to check whether such a trivial derivation exists. Lemma 10.16. Given a ^-language j(w,C), a PRS system A, and constants X, Y, the following problems are decidable: (i) Is there any derivation X -^->* Y satisfying 7(10, C)? Hi) Is there any derivation X -^->* t such that t is a term and u G 7(10, C) ľ Proof. Both problems can be reduced to the reachability problem for wPRS (i.e. to decide whether given states p\t\, P2Í2 of a given wPRS system A' satisfy piti —>*A, P2Í2 for some v), which is known to be decidable (Theorem 8.8). (i) Let w = a\0\... anOn. We construct a wPRS A' with the set of control states {l,2,...n}U2c. We use {n +1) as another name for the control state 0 (from 2C). The set of rewrite rules is defined as follows. • For every 1 < i < n and every rule ii ■—> í2 of A, we add to A' the rule it\ ■—> (í + 1)Í2 and if Oi = U+ then also the rule it\ c-^ Ü2. • For every b G C, every D C C, and every rule 11 °-> 12 of A, we add to A' the rule Dtľ ^(DU {b})t2. Obviously, a word u G Act* satisfies IX —>*A, CY if and only if it satisfies both X -^->*A Y and u G 7(10, C). As we can decide whether IX -^*A, CY holds for some u, we can decide Problem (i). (ii) We construct a wPRS A' as in the previous case. Moreover, for every Z G Const(A) we add to A' the rule C Z c-^ Ce. It is easy to see that if a word u *A t for some t, then IX ^U*A, Ce holds for some m > 0. Conversely, if IX —>*A, Ce holds for some v, then some prefix u of v satisfies both u G 7(10, C) and X —>*A t for some t. As we can decide whether IX —>*A, Ce holds for some v, we can decide Problem (ii). D The proof of the following lemma contains an algorithmic core of this section. 124 LINEAR TIME LOGIC Lemma 10.17. Let A be a PRS in normal form and ß(w,B,C) be a ß-formula. One can construct a PRS A' in flat (w, B, C)-form such that, for each («/, B', C) c (w, B, C) and each X e Const(A), is holds that in A' there is an infinite derivation starting from X and satisfying ß(w', B', C') if and only if in A there is an infinite derivation starting from X and satisfying ß(w', B', C'). Proof In order to obtain A', we describe an algorithm extending a PRS A with trivial rewrite rules according to Conditions 1-5 of Definition 10.14. All the conditions of Definition 10.14 can be checked for each X,Y e Const(A), each («/, B', C) C (w, B, C), and each B" C B. For Conditions 1 and 2, this follows from Lemma 10.16. For Condition 3, a problem whether there is an infinite derivation X —>w satisfying ß(£,B',C') is a special case of the fairness problem - see Proposition 10.15, which is decidable due to [Boz05]. Finally, Conditions 4 and 5 can be checked due to decidability of LTL model checking for PDA and PN. Hence we can check if the conditions are satisfied. If there is a derivation which violates some of the conditions, we add some trivial rules to ensure the existence of a trivial derivation required by the respective condition. This process of adding new trivial rules is described in what follows. Let us assume that Condition 3 (or 4 or 5) is not satisfied, i.e. there exists an infinite derivation X —>w (or X —> ^ar or X —> ^eq respectively) satisfying ß(w', B', C) for some («/, B', C) C (w,B,C) and violating the condition. Remark 10.12 implies that C is nonempty and there is a finite derivation X -—^ t satisfying 7(10', B'). Hence, there exists an ordering of B' = {bi, 62, • • •, bm} such that (*) for each 1 < j < m, there is a finite derivation in A starting from X and satisfying j(w', {b\,..., bj}). Such an ordering can be effectively computed using Lemma 10.16. Further, let w' = a\ö\a2Ö2 ■ ■ ■ anOn and let C = {c\, C2,..., Ck}. Then, we add the trivial rule Zj_i <—► Zi for each 1 < i < n, the trivial rule Zra+j_i ^-> Zn+j Cj for each 1 < j < m, and the trivial rule Zn+m+j_i c-^ Zn+m+j for each 1 < j < k, where Z0 = X, Z\,..., Zn+m+k_i are fresh process constants, and Zn+m+k = Zn+m. These added rules form an infinite derivation using only trivial rules, starting from X, and satisfying ß(w', B', C). Similarly, if there are X, Y, and 7(10', B") with w' = a\ö\a2Ö2 ■ ■ ■ anOn such that Condition 1 or 2 of Definition 10.14 is violated, then we first compute an ordering {61,..., bm} of B" satisfying (*), and then we add the trivial rule Zj_i ■—> Z i for each 1 < i < n, and the trivial rule Zra+j_i "-^ Zn+j 10.4 MODEL CHECKING OF wPRS AGAINST NEGATED A 125 for each 1 < j < m, where Zq = X and Z\,..., Zn+m are fresh process constants (with exception of Zn+m which is Y in the case of Condition 1). ai...a„bi...bm The added trivial rules generate derivation X —>* Zn+m satisfying 7(«/, B"). Note that Conditions 1 and 2 are always satisfied if n = m = 0 as7(e,0) = {e}. Let A" be the PRS A extended with the new rules. The condition (*) ensures that, for each X e Const(A) and each («/, B', C') C (w, B, C), A" is equivalent to A with respect to the existence of an infinite derivation starting from X and satisfying ß(w', B', C). If A" is not in flat (w, B, C)-form, then the algorithm repeats the procedure described above on the system A" with the difference that X and Y range over the constants of the original system A. The algorithm eventually terminates as the number of iterations is bounded by the number of pairs of process constants X, Y of A, times the number of triples («/, B', C) satisfying («/, B', C) C (w, B, C), and times the number of subsets B" C B. We claim that the resulting PRS A' is in flat (w,B, C)-form. By the construction, A' satisfies all conditions of Definition 10.14 for the process constants of the original system A. For the added constants, it is sufficient to observe that any derivation in A', starting from such a constant, is either trivial or it has a trivial prefix leading to a constant of A. Hence, A' is the desired PRS system. D Definition 10.18 (Subderivation). Let Abe a PRS in normal form and a\ be a {finite or infinite) derivation s\ —U- S2 —^ ..., where s\ —U- S2 has the form X —U- Y.Z and, for each i > 2, if Si is not the last state of the derivation, then it has the form Si = U.Z with U / e. Then u\ is called a subderivation of a derivation a if a has a suffix a1 satisfying the following: 1. every transition step in a' is of the form Si\\ť -^-> Si+i||i' or Si\\ť —> Si\\t"', where ť —► t", 2. in a', if we replace every step of the form Si\\ť -^-> Si+i||i' by step Si -^ Si+i and we skip every step of the form Si\\ť —► Si\\t", we get precisely a\. Further, if a\ and a are finite, the last term of a\ is a process constant, and a is a prefix of a derivation a', then a\ is also a subderivation of a'. Remark 10.19. Let A be a PRS in normal form and a be a derivation of A having a suffix a' of the form a' = X\\t —> (Y.Z) \\t —ť . Then, there is a subderivation of a whose first transition step X -^-> Y.Z corresponds to the first transition step of a'. Intuitively, a subderivation captures the behaviour of the subterm Y.Z since its emergence until its eventual reduction to a term without any se- 126 LINEAR TIME LOGIC quential composition. Due to the normal form of A, the subterm Y.Z behaves independently on the rest of the term (as long as it contains a sequential composition). Lemma 10.20. Let Abe a PRS in flat (w, B, C)-form. Then, the following condition holds for each X e Const(A) and each («/, B', C) c (w, B, C): If there is an infinite derivation X -^w satisfying ß(w', B', C), then there is also an infinite derivation X -—^ri satisfying ß(w', B', C'). Proof In the following two paragraphs, we provide a sketch of the proof. The full proof follows. Given an infinite derivation a satisfying a formula ß(a) = ß(w', B', C) where (w', B', C') C (w,B,C),by trivial equivalent of a we mean an infinite trivial derivation starting in the same term as a and satisfying ß(a). Similarly, given a finite derivation a satisfying some 7(a) = 7(11/, B') where («/, B') C (w,B),by trivial equivalent of a we mean a finite trivial derivation a' such that a' starts in the same term as a, it satisfies 7(a), and if the last term of a is a process constant, then the last term of a' is the same process constant. The lemma is proven by contradiction. We assume that there exist some infinite derivations violating the condition of the lemma. Let a be one of these derivations such that the number of transition steps of a generated by sequential non-trivial rules with actions a <£ B is minimal (note that this number is always finite as we consider derivations satisfying ß(w', B', C') for some («/, B', C) C (w, B, C)). First, we prove that every subderivation of a has a trivial equivalent. Then we replace all subderivations of a by the corresponding trivial equivalents. This step is technically nontrivial because a may have infinitely many subderivations. By the replacement we obtain an infinite derivation a' satisfying ß(a) and starting in the same process constant as a. Moreover, a' has no subderivations and hence it does not contain any sequential operator. Flat (w,B, C)-form of A (Condition 4) implies that a' has a trivial equivalent. This is also a trivial equivalent of a which means that a does not violate the condition of our lemma. In this proof, by /3-formula we always mean a formula of the form ß(w', B', C) where (w', B', C) C (w, B, C). We also consider only infinite derivations satisfying some of these /3-formulae. Remark 10.13 implies that such an infinite derivation a satisfies exactly one /3-formula. We denote this /3-formula by ß(a). Further, by SEQ(a) we denote the number of transition steps t i —► čj+i of a generated by a sequential non-trivial rule and such that a £ B. Note that SEQ(a) is always finite due to the restrictions on considered infinite derivations. Given an infinite derivation a, by its trivial equivalent we mean an infinite trivial derivation starting in the same term as a and satisfying ß(a). 10.4 MODEL CHECKING OF wPRS AGAINST NEGATED A 127 Similarly, we consider only finite derivations satisfying some 7(11/, B') where («/, B') C (w, B). Remark 10.13 implies that such a finite derivation a satisfies exactly one 7-language, which is denoted by 7(a). Given a finite derivation a, by its trivial equivalent we mean a finite trivial derivation a' such that a' starts in the same term as a, it satisfies 7(c), and if the last term of a is a process constant, then the last term of a' is the same process constant. Using the introduced terminology, the lemma says that every infinite derivation starting in a process constant has a trivial equivalent. For the sake of contradiction, we assume that the lemma does not hold. Let X be the set of infinite derivations violating the lemma and let k = mm{SEQ(a) \ ctGS}. First of all, we prove two claims. Claim 1. Let a be an infinite derivation satisfying SEQ(a) < k. Then every subderivation of a has a trivial equivalent. Proof of the claim: For finite subderivations, the existence of trivial equivalents follows directly from the flat (w, B, C)-form of A (Conditions 1 and 2). Let (7i be an infinite subderivation of a. It has the form (Ti = X —>seq Y.Z —>t\.Z —>t2-Z —►... where či, Č2, • • • are nonempty terms. There are two cases: • If a G B, then ß(a{) has the form ß(e, B', C"). Hence, a\ has a trivial equivalent due to the flat (w, B, C)-form of A (Condition 3). If a g" B, then the first step X —>seq Y.Z of o\ is counted in SEQ(a\) and the corresponding step X\\ť —>seq Y.Z\\ť of a is counted in SEQ(a). Hence, 0 < SEQ(a). Let a2 be the derivation (72 = F ------> Či ------> Č2 ------> . . . As SEQ(g2) < SEQ(ai) < k, the definition of k implies that 02 has a trivial equivalent seq Y.Z ----->tri Y\.Z ----->tri Y2.Z ----->tri ■ ■ ■ satisfies ß(a{). Moreover, the flat (w,B, C)-form of A (Condition 5) implies that a[ has a trivial equivalent. Obviously, it is also a trivial equivalent of a\. D 128 LINEAR TIME LOGIC Claim 2. Let a be an infinite derivation such that SEQ(a) < k, it starts in a parallel term p, and it satisfies a formula ß(w',B',Cr). Then there is an infinite derivation p -—>■ *par p' -—>■w such that p' is a parallel term, u G 7(«/, B'), and v satisfies ß(e, C, C). Proof of the claim: Remark 10.12 implies that a can be written as p —V t —^ 0 where p —^* t is the minimal prefix of a satisfying 7(10', B') and such that t —^w satisfies ß(e, C, C). Let SEQ(a) denote the number of transition steps in the prefix p —^* t generated by sequential non-trivial rules (note that ŠEQ(a) > SEQ{a)). We prove the claim by induction on ŠEQ(a). The base case SEQ(a) = 0 is obvious. Now, assume that SEQ(a) > 0. Since p is parallel term and A is in normal form, the first transition step of p —V t counted in SEQ(a) has the form Y\\p' -^-> (M^.Z)||p' and it corresponds to the first transition step Y -% W.Z of a subderivation <7i. In a, we replace the subderivation <7i with its trivial equivalent (whose existence is guaranteed by Claim 1) and we obtain a new derivation a" starting from p, satisfying ß(a) and such that SEQ(a") < SEQ(a). Hence, the second claim directly follows from the induction hypothesis. In the following, we describe the replacement of such a subderivation. Let ai = Y -^w and a[ = Y -^fri be its trivial equivalent. Let ß(ai) = ß{clOic202...cnOn,B",C"). Then u, v G c+c+ ...c+.B". Recall that ci, C2,..., cn are pairwise distinct and B C Act \ {c\,..., cn}. Intuitively, for every 1 < i < n, we replace the first transition step of a\ labelled with Ci by the sequence of transition steps of a[ labelled with Cj, and then we cancel the other transition steps of a\ labelled with c^.5 Further, the first transition step of a\ labelled with an action of B is replaced with the minimal prefix of the remaining part of a[ satisfying 7(5:, B"). Finally, the remaining transition steps of a\ are orderly replaced with the remaining transition steps of a[. The case when a\ and its trivial equivalent a[ are finite is similar. It is easy to see that the described replacement operation preserves the fulfilment of ß(a) and the obtained derivation a" satisfies SEQ(a") < SEQ(a). D With this claim, we can easily reach a contradiction. Let a = X —^ be an infinite derivation such that SEQ(a) = k and it has no trivial equivalent. 5By replacement of a transition step si -^-> S2 of o\ by a sequence Y\ -^*ri Yi of transition steps of a[ we mean that the corresponding transition step sip' -^-> S2p' of a is replaced by Yi\\ť -^*ri Vbp', and all immediately succeeding steps S2p" —► s2p"/ of a ate replaced by I2P" —► Y2\\ť". Further, by cancellation of a transition step si —^ S2 of ai we mean that the corresponding transition step si \\ť —^ S2 \\ť of a is replaced by I2 \\ť, where I2 is the last process constant of a[ such that a transition under Ci leads to I2, and all immediately succeeding steps S2 \\t" —> S2 \\ť" of a are replaced by I2 \\t" —> I2 \\ť". 10.4 MODEL CHECKING OF wPRS AGAINST NEGATED A 129 Further, let ß(a) = («/, B', C). Note that C is nonempty. Claim 2 says that there is a derivation X —^*par Pi -^w where p\ is a parallel term, v,\ e 7(«/, B1), and vi satisfies ß(e, C, C). Applying the second claim on the suffix p i —L->^ , we get a derivation pi —^>Par P2 —^ where P2 is a parallel term, -U2 e 7(e, C"), and ^2 satisfies ß(e, C, C). Iterating this argument, we get a sequence (pi -:—^*par Pi+i)ien of derivations satisfying j(e, C). These derivations are nonempty as C is nonempty. Let us consider the derivation / __ y U\ * U2 ^ _«3 * «4 ^ " -^ par Pi par "2 par P3 par • • • Flat (w,B, C)-form of A (Condition 4) implies that a' has a trivial equivalent. However, this is also a trivial equivalent of a as both a, a' start with X and a' satisfies ß{a). This is a contradiction. D Theorem 10.21. The problem whether a given PRS A in normal form has an infinite run satisfying a given formula ß(w, B, C) is decidable. Proof. Due to Lemma 10.17 and Lemma 10.20, the problem can be reduced to the problem whether there is an infinite derivation X —>fri satisfying ß(w, B, C). This problem corresponds to LTL model checking of finite-state systems, which is decidable. D The following three theorems show that Theorem 10.21 holds even for wPRS and a-formulae. Theorem 10.22. The problem whether a given PRS A in normal form has an infinite run satisfying a given a-formula is decidable. Proof. Let A be a PRS in normal form and ot{9\0\... 9nOn(, B) be an en-formula. For every 9i and every rule či °-> Č2 such that b satisfies 9i, we add a rule či ■—> Č2, where a» is a fresh action corresponding to 9i. Similarly, for every ip e £> U {{} and every rule či °-> í 2 such that b satisfies ip A £, we add a rule či °-> Č2, where a^ is a fresh action. Let A' be the resulting PRS system. Note that A' is also in normal form. Obviously, A has an infinite run satisfying the original a-formula if and only if A' has an infinite run satisfying a(aiOi... anOn(a^ V \/beC b),C), where C = {a^ \ ip e B}. It is an easy exercise to show that this new a-formula can be effectively transformed into a disjunction of /3-formulae which is equivalent with respect to infinite words. Hence, the problem is decidable due to Theorem 10.21. D Theorem 10.23. The problem whether a given PRS A has an infinite run satisfying a given a-formula is decidable. 130 LINEAR TIME LOGIC Proof. Let A be a PRS, a(ö, B) be an a-formula, and e ^ Act (A) be a fresh action. First we describe our modification of the standard algorithm [MayOO] that transforms A into a PRS in normal form. If A is not in normal form, then there exists a rule r which is neither parallel nor sequential; r has one of the following forms: 1. r = t °-> íi ||č2 (resp., r = t\ ||č2 °-*-1) where t or či or č2 is not a parallel term. Let Zi, Z2, Z qL Const (A) be fresh process constants. We replace r with the rules t c-^ Z, Z c-^ Zi||Z2, Z\ c-^ t\, and Z2 c-^ č2 (resp., íi ^ Zx, i2 A Z2/ Zi ||Z2 ^ Z, and Z A í). 2. r = í A íi.(í2||Í3) (resp., r = či.(č2||č3) ^ í)- Let Z $_ Const(A) be a fresh process constant. We modify A in two steps. First, we replace Í2IIÍ3 by Z in left-hand and right-hand sides of all rules of A. Then, 6 6 we add the rules Z ^-> č2||Č3 and í211 í3 "—>■ Z. 3. r = íi °-> č2.X (resp., r = č2.X "-^ či) where či or č2 is not a process constant. Let Z\, Z2 ^ Const (A) be fresh process constants. We replace r with the rules či °-> Zi, Zi °-> Z2.X, and Z2 ^-> č2 (resp., Č2 ^ Z2, Z2.X A Zi, and Zx A či). After a finite number of applications of this procedure (with the same action e), we obtain a PRS A' in normal form. We define a formula a(ö', B'), where B' = £>U {V«eAcŕ(A) a) an(^ ^' arises from ö = 9\0\... 9nOn( by the following substitution for every 1 < i < n. • If Oi is U, then replace the pair 6i U by the pair (e V 6i) U . • If O i is U+, then replace the pair 6 i U+ by the sequence (e V 6 i) U 6 i U+ . • If Oi is A X, then replace the pair Q i A X by the sequence e U 0j A X. • dnOn = 6n A Gs is replaced by the sequence e U 0n A Gs. • £ is replaced by (£ V e). Let us note that the construction of £>' ensures that any word with a suffix ew does not satisfy a(ö', B'). Observe that u' |= a(ö', B') if and only if u |= a(ö, B), where u is obtained from v! by eliminating all occurrences of action e. Clearly, A has an infinite run satisfying a (ô, B) if and only if A' has an infinite run satisfying a(ö', B'). As A' is in normal form, we can now apply Theorem 10.22. D Theorem 10.24. The problem whether a given wPRS system has an infinite run satisfying a given a-formula is decidable. 10.5 MODEL CHECKING LTL(FS, Ps) 131 Proof. Let A be a wPRS with initial state poXo and a(ö, B) be an a-formula. We construct a PRS A' with initial state Xo which can simulate A. We also define set of formulae recognising correct simulations. The system A' is very similar to A. We only change actions of rules to hold information about control states in the rules and then we remove all control states. More precisely, for every rule of the form pt\ c-^ pt2 of A we [pi ft, add to A' the rule či °-> Č2, and for every rule of the form pt\ °-> $2 of A we add to A'the rule č 1 °-> Č2. Further, we modify the formula a (ô, B) such that every occurrence of each action a is replaced by VgeM(A) (aM v VP<9 a[pi A Y(ipi S ^2)- Now, we can define a past variant of the A fragment called VA. Definition 10.26. Let rj = L1P1L2P2 ■ ■ ■ im,Pm^m+i, where • m > 0, • Lj G LTL() for each j < m + 1, • Pj is either 'S' or 'S+' or 'A Y' /or eac/z j < m, and • Pm is 'A Hs'. Similarly, let 5 = 9\0\9202 ■ ■ ■ 0nOn9n+i, where • n > 0, • 0i G LTL() for each í < n + 1, • Oj is ez'ŕ/zer 'U' or 'U+' or 'AX' /or eac/z í < n, and On iS 'AGs'. Further, let B c LTL() be afinite set. A Pa-formula zs defined as Pa(r], 6, B) = (tiPi(t2-P2 • • • (im-PmWi) • • •)) A a {e1o1(e2o2■ ■ ■ (enonen+i)...)) a /\^eBgsfs^ The VA fragment consists of finite disjunctions of Pa-formulae. Intuitively, Pa-formula Pa(r], 6, B) is an a(ö, B) extended with a new conjunct that describes a past part. Hence, rj is a past counterpart of 6. There is no past counter part to A^,eßGsFs^ as every history is finite — it begin in the initial state. Therefore, a pointed word (u, k) satisfies Pa(r], ö, B) if and only if (u, k) satisfies a(ö, B) and «(0)... u(k — l)u(k) can be written as Vm+i.Vm-i. ■ ■ ■ .V2.V\ where each Vi, for i = 1,..., m + 1, consists only of actions satisfying ti and • \vi\ > 0 if i = m + 1 or Pi is 'S', • \vi\ > 0 if Pi is 'S+', • \vi\ = lif P is'AY'or 'AHS'. In the following lemmata we provide a list of operation under which the VA fragment is closed. Proofs of the lemmata are easy but sometimes very technical exercises, hence we sketch their basic ideas only. 10.5 MODEL CHECKING LTL(FS, Ps) 133 Lemma 10.27. A conjunction of Pa-formulae can be effectively converted into a globally equivalent disjunction of Pa-formulae. The proof is constructed in a similar way as the proof of Lemma 10.9. Lemma 10.28. Let ipbea Pa-formula. A formula X

5), the set Av can be constructed from AqspsIP3 and fsip5 using Lemma 10.27. 10.5 MODEL CHECKING LTL(FS, Ps) 135 *PS Case GSFS((^3 A Ps^5): As GSFS(^3 A Ps^5) = (GSFS^3) A (GSFSPS^5), the set Av can be constructed from AQspslp3 and AqspsPsV6 using Lemma 10.27. *GS Case GSFS(^3 A Gs^5): As GSFS(^3 A GsLp5) = (GSFS^3) A (GSFSGS^5), the set Av can be constructed from AQspslp3 and AqspsqsIP5 using Lemma 10.27. *HS Case GsFs(t£>3 A Hs^5): As GsFs(t£>3 A Hs^5) = (GSFS^3) A (GsFsHst£>5), the set Av can be constructed from AQspslp3 and Aqspsp\sV6 using Lemma 10.27. -Fs Case GsFsFst£>3: As GsFsFst£>3 = GSFS(^3, we set A^ = AGspsip3. —Ps Case GsFsPs(/?3: A pointed word (u, i) satisfies GsFsPst£>3 iff i = \u\ — 1 or u is an infinite word satisfying Ft£>3. Note that Gs—iŕŕ is satisfied only by finite words at their last position. Further, a word u satisfies (Fsřř) A (GsFsŕŕ) iff u is infinite. Thus, GSFSPS(^3 = (Gs-iřř) V Lp' where Lp' = (Fsřř) A (GsFsŕŕ) A (^3 V Ps<ŕ>3 V Fs^3). Hence, Av = Aqs^h U A^ where A^ is constructed from Apstt, AQspstt, and A^3 U ApsLp3 U ApsLp3 using Lemma 10.27. —Gs Case GSFSGS(£>3: A pointed word (u, i) satisfies GSFSGS(£>3 iff i = \u\ — 1 or u is an infinite word satisfying FSGS(£>3. Thus, GSFSGS^3 = (Gs-.ŕŕ)V where Lp' = (Fsřř) A(GsFsřř) A(FSGS^3). Hence, Av = Aq^^uA^ where A^ is constructed from Apstt, AqspsU/ and ApsQsV3 using Lemma 10.27. —Hs Case GsFsHst£>3: A pointed word (u,i) satisfies GsFsHst£>3 iff i = \u\ — 1 or u is an infinite word satisfying G(£>3. Thus, GSFSHS^3 = (Gs--řř) V Lp' where Lp' = (Fsřř) A (GsFsŕŕ) A (3): According to the structure of Lp2 and Lp3/ there are the following subcases. -k'P Case Gs('[)2 Vp3): As P2 Vp3 e LTL(), this subcase has already been covered by Case Gsp. ■kf\ Case Gs(Lp2\/((pi f\Lp5)): As Gs(Lp2V^At^)) = Gs(Lp2 V^) A Gs{lp2 y ip5), the set Av can be constructed from ^-Gs^v^m) and AGs(¥,2V¥,B) using Lemma 10.27. *FS Case Gs((£>2 V Fs2 V Fs^4) = (Gs^2) V FS(FS(^4 A GsLp2) V GsFsLp4. Therefore, the set Av can be constructed as AQsV2 U ^fs(fs¥>4ags¥>2) U AqspsVa, 136 LINEAR TIME LOGIC where ^fs(fs¥>4ags¥>2) is created from AfsV4 and AGsip2 due to Lemma 10.27 and Lemma 10.32. *HS Case Gs(4) where AFs{Hsip4AGsip2) can be created from A^s(p4 and AG sip2 using Lemma 10.27 and Lemma 10.32. *GS, Ps Case Gs(ip2 V Gsip4 V Ps^s): There are only the following five subcases (the others fit to some of the previous cases). (i) Case Gs(V^eG Gs^): It holds that Gs(V^eG Gsif/) = (Gs—iŕŕ) V \f ,eG(XGs' where each AXGsip' is created from AGsip> using Lemma 10.28. (ii) Case Gs(p2 V V^ec W): As Gs(p2 V V^ec G^0 = (Gsp2) V V¥,/€g(x(P2 U (Gsy/)))- Therefore, the set A^ can be constructed as AGsP2 uU^c ^X(P2 u (Gs¥/)) where each ^4x(p2 u (Gs¥/)) ^s created from AGs(p/ using Lemma 10.30 and Lemma 10.28. (m) Case Gs(V^/eP Ps^"): It holds that Gs(V^/eP RVO = (Gs-iřř) V V^'ep(xps^')- Therefore, the set ^ can be constructed as AGs^tt U {j!p„eP Axps(f" where each Axps(f" is created from Apsip» using Lemma 10.28. {iv) Case GS(P2 V V^eP Psy"): As Gs(p2 V V^eP Ps^') = (GsP2) V V^ep(X(P2U(Ps^"))). Therefore, the set Ay, can be constructed as AGsP2 U U^'ep ^X(P2 u (Ps¥/')) where each ^x(p2 u (R^")) is created from Aps¥// using Lemma 10.30 and Lemma 10.28. (v) Case Gs(p2 V \/^,eGGsV' V \/^,eP Pstp"): As GS(P2 V V^eGGs^ V M^pGsv") = (Gsp2) V V^eG(X(p2 U (Gs^))) V V^ep(X(P2 U (Ps¥>"))). Therefore, the set A^, can be constructed as ^GsP2 U U^eG^XÍpalKGs^/)) U U^'eP ^X(p2 U (Ps¥/')) where each ÁX(P2 u (Gs¥/)) is created from ^gs¥/ and each Ax(P2 u (Ps^")) is created from Aps¥// using Lemma 10.30 and Lemma 10.28. oGs Case GsGst£>2: As GS(GS2: A pointed word (u,i) satisfies GS(HS^2) iff i = \u\ — 1 or (u, \u\ — 1) satisfies Hs^2 or u is infinite and all its positions satisfy 2)a^2a(gs¥)2) is created from AGs^tt, A\\sLp2, A^, and AGsip2 using Lemma 10.27 and Lemma 10.32. 10.5 MODEL CHECKING LTL(FS, Ps) 137 ►Hs Case Hs^i: This case is divided into the following subcases according to the structure of 2: A pointed word (u, i) satisfies HsFst£>2 iff i = 0 or (u, i) satisfies F^2- Note that Hs—iŕŕ is satisfied by (u, i) only if i = 0. Therefore, Av = A^S^H U AV2 U ApsV2. oPs Case HsPst£>2: Every run has to start in the initial state, and so, every history is finite. Hence, a pointed word (u, i) satisfies HsPst£>2 iff í = 0. Therefore, Av = A^s-,tt. oV Case Hs(t£>2 V (ps): According to the structure of 2)- Therefore, the set Av can be constructed as AHs¥,2 U Aps(Ps¥,4AHs¥,2), where Aps(Ps¥,4AHs¥,2) is created from Apsip4 and A\-\sip2 due to Lemma 10.27 and Lemma 10.33. *GS Case Hs(^2 V Gs^4): As Hs(^2 V Gs^4) = (Hs^2) V Ps(Gs^4 A Hs(^2). Hence, A^ is constructed as AHsip2 U APs(Gs¥,4AHs¥,2) where ^ps(gs¥>4ahs¥>2) is created from AGs(p4 and AHs¥,2) using Lemma 10.27 and Lemma 10.33. *FS, Hs Case Hs(^2 V Fst£>4 V Hs^5): There are only the following five subcases (the others fit to some of the previous cases), (i) Case Hs(V¥,/eF Fs¥>'): It holds that Hs(V¥,/eF Fs is created from Aps(p> using Lemma 10.29. (ii) Case Hs(p2 V V^f Fsp'): As Hs(p2 V V^f Fsp') = (Hsp2) V V'v,(zF(y(p2 S (FsW): It holds that Hs(V^/eH >W) = (Hs-.řř) V V «"eířC^^s^")- Therefore, the set Av can be constructed as A\\s^n\Wipl,eH ^yhs¥/' where each Ay^s(p» is created from A\\sipn using Lemma 10.29. 138 LINEAR TIME LOGIC (iv) Case Hs(p2 V V^/'eŕŕ Hst£>"): As Hs(p2 V V«"eii (Hsp2) V V^'eH(Y(P2S(Hs^"))). Therefore, the set Av can be constructed as AHsP2 U U^'gjí ^y(P2s(hs¥/')) where each ^4y(p2s(hs^")) is created from A^» using Lemma 10.29 and Lemma 10.31. (v) Case Hs(p2 V \/^phtf V V^es Hs¥>"): As HS(P2 V V^efFs^' v V^eí/Hs^O = (Hsp2) V V<^(Y(P2 S (Fs^))) V V^en(Y(P2 S (Hs¥>"))). Therefore, the set A^, can be constructed as AHsP2 U U^'eF^YÍpaSÍF^')) U IV e Jí AY(P2 S (Hs¥/')) where each Ay^s^')) ^s created from Aps¥/ and each ^Y(p2s(Hs¥)")) is created from A^sip// using Lemma 10.31 and Lemma 10.29. oGs Case HSGS(£>2: A pointed word (u,i) satisfies HS(GS(£>2) iff i = 0 or («, 0) satisfies Gs2)) where ^ps((Hs-ft)A(Gs¥!2)) is created from AHs^tt and AQsV2 using Lemma 10.27 and Lemma 10.33. oHs Case HsHst^2: As Hs(Hst^2) = (Hs-.ŕŕ) V (YHS^2), the set A^ can be constructed as A^s-,tt U AyhS(p2 where AyhS(p2 is created from Ah sip2 using Lemma 10.29. D In other words, we have shown that LTL(FS, Ps) is a semantic subset (with respect to global equivalence) of every formalism that is able to express p where p G LTLQ, • Gsp where p G LTLQ, • Hsp where p G LTLQ, and • GsFsp where p G LTLQ and is closed under • V operation, • A operation, • X application, • p U application where p G LTLQ, • Y application, and • p S application where p G LTLQ. 10.5 MODEL CHECKING LTL(FS, Ps) 139 Now, using Theorem 10.11 and Theorem 10.24 we can easily proof decidability of the model checking problem for wPRS and negated formulae of the VA fragment. In fact, we prove decidability of the dual problem, i.e. whether a given wPRS system has a run satisfying a given formula of VA. Theorem 10.35. The problem whether a given ivPRS system has a run satisfying a given Pa-formula is decidable. Proof. A run over a word u satisfies a formula

, R,po,to) be a wPRS and pt be a reachable nonterminal state of A. We construct a wPRS A' = (M, >, R',p0,t0.X) where X <£ Const(A) is a fresh process constant, / ^ Act (A) is a fresh action, R' = RU {(p(t.X) A pXa), (pXa £ pYa), (pYa A p>ť) I pt -^a p't'}, and Xa, Ya ^ Const(A) are fresh process constants for each a G Act (A). It is easy to see that (u, i) is in L(pt, A) if and only if tt(0)«(l).. .u(i — l)u(i). f .u(i) .u(i + 1)... is in L(A'). Hence, for a given Pa-formula if = Pa(rj, ö, B) we construct a Pa-formula ip' = Pa(r], tt A X/ A Xö, B). We get that L(pt, A) |= Pa(r], 6, B) ^^ L(A') |= F(Pa(r?, tt A X/ A X6, B)) and due to Lemma 10.30 and Theorem 10.35 the proof is done. D 140 LINEAR TIME LOGIC As LTL(FS, Ps) is closed under negation and Theorem 10.34 works with global equivalence, Theorem 10.37 give us the following. Corollary 10.38. The pointed model checking problem is decidablefor wPRS and LTL(FS, Ps). 10.6 Undecidability Results In this section we prove that the model checking problem is undecidable oo for the PA class and the fragments LTL(U) and LTL( F, X), respectively. The undecidability proofs are based on reduction from the non-halting problem for Minsky 2-counter machines, which is known to be undecidable [Min67]. See Subsection 7.3.2 for the Minsky 2-counter machine definition. Theorem 10.39. The model checking problem for PA and LTL(U) is undecidable. Proof. Given a machine N = h : i\, I2 : Í2, ■ ■ ■, In-i '■ in-i, In '■ halt, we construct a PA system An with the initial term D\ \\Ľ2\\H. In what follows we construct sets of rewrite rules emulating instructions of the machine N. Moreover, for each instruction, we define an LTL formula describing a correct simulation of the instruction in the PA system. Increment: k: c^: = c^+l; goto lr To each such an increment instruction of the machine N we add to A the following rules: Dk '-^ Sk-Dk Ck "-^ Sk-C'k Sk °-> C'k.Sk The correctness formula ipi of this instruction is as follows: (k => (h U inci)) A (inci ^=> (inci U lr)). Intuitively, it says that every k action is followed by the inci action that has to be followed by the lr action. Test-and-decrement: Zi:if Cfc>0 then Cfc: = Cfc-l; goto lr else goto ls To each such a test-and-decrement instruction of the machine N we add to A the following rules: Zi zeroi li deci Dkc-^ Ek Ek °-> Dk Ckc-^> £ Sk "-^ £ 10.6 UNDECIDABILITY RESULTS 141 The correctness formula ipi of this test-and-decrement instruction is as follows: (k =^ (k U (deciVzeroi))) A (deci ==> (deci U k)) A (zeroi ==> (zeroi U ls)). Intuitively, it says that every k action is followed by the deci action or the zeroi action. Moreover, the two last conjuncts express that the actions deci and zeroi has to be followed by the k and ls, respectively. Halt: ln-.halt The halt instruction is translated into the following rule: Finally, we define a general formula if as follows:

i)Vln). l Xlr). Intuitively, it says that every k action is followed by the inci action that has to be followed by the k action. 142 LINEAR TIME LOGIC Test-and-decrement: Zi: if Cfc>0 then Cfc: = Cfc-l; goto lr eise goto ls To each such a test-and-decrement instruction of the machine N we add to A the following rules: zeroi deci Dk c-^ Dk Gfc "-^ e The correctness formula ipi of this test-and-decrement instruction is as follows: (k ==> X(deci V zeroij) A (deci ==> X/r) A (zero» ==> XZS). Intuitively, it says that every U action is followed by the deci action or the zeroi action. Moreover, the two last conjuncts express that the actions deci and zeroi has to be followed by the lr and ls, respectively. Halt: Zn:halt The halt instruction is translated into the following rules. H c—> H H c—> H for every 1 < i < n Restart: Additionally, we also add the rules enabling to reset the counters. deli „ deh „ reseti reset2 „ Ci ^ e C2 ^> e Di ^ Di D2 <^> D2 As in the previous proof, we define a formula ip which describes a correct step of the constructed PA system when simulating machine N. tp = f\ tpi A (ln => Xhalt) l X(dd\ V reseti)) A (deli => X(deli V reseti)) A (reseti => X(del2 V reset2)) A (del2 ==> X(del2 V reset2)) A (reset2 ==> XZi) 10.7 SUMMARY 143 The formula

H by the rule H ■—> ein the proof of Theorem 10.39. Remark 10.43. As all the systems of the extended PRS-hierarchy are finitely branching, the number of states reachable in a given finite number of steps is finite. Therefore, it can be easily shown that the model checking problem is decidablefor LTL(X) and sePRS. Remark 10.44. However, note that model checking of finite runs against oo ĽTL( F, X) is decidable, even for wPRS. The proof is based on the observation that oo a nonempty finite run satisfies ftp if and only if the last action of the run satisfies oo p. The same holds for a formula Gp. Hence, if we restrict only to nonempty finite oo oo oo runs, the modalities F, G are equivalent. The observation also implies that F -*

H is replaced by H <—> e, the "reset" rules are needless, and the formula

halt) U halt, the LTL model checking problem is undecidable for all Turing powerful classes, i.e. sePA and all its superclasses. Using some of the ideas of [MaiOO] and decidability of the model checking problem for LTL(FS, Gs) and wPRS, we show that the model checking problem for wPRS and LTLdet is decidable. Note that LTLdet is semantically incomparable with LTL(FS, Gs). 150 LTLUhl MODEL CHECKING 11.2 Definition of the Studied Problem To define LTL , we use the (common) LTL modalities X, U, F, G, etc. as they have been defined in the previous chapter (see Definition 10.4 and Figure 10.1). In addition, we introduce another LTL modality W. Definition 11.1. Weak until modality W is defined using U and G as ip\Nip = Gtf V pi \ p\ Ap2, and a ranges over Act. The semantics of LTL formulae is interpreted over both finite and infinite words of actions in the same way as it was defined in Definition 10.4 in the previous chapter. Weak Automaton In this chapter, we make use of Büchi automata to represent LTL formulae. We define an automaton as follows. Definition 11.3. An automaton1 A = (Q, E, qo, R, F) over the alphabet E consists of: • the finite set of states Q, • the initial state qo G Q, • the transition relation R c Q x E x Q, and • the set of accepting state F Q Q. A weak automaton is an automaton such that there is a partial ordering > on the states of Q such that every q and q' for which (q, q') G R, we have q > q'. :An automaton differs from (LTS generated by) FS class just by having accepting states. The same is true for a weak automaton and a weak FSU. 11.3 PROOF CONSTRUCTION 151 A run of A over a word u = u(0)u(l)u(2)... G E* U Ew is a sequence a = q(0)q(l)q(2)... G Q+ U Q" such that q(0) = q0 and for all i > 0, (q(i),u(i), q(i + 1)) G R. An infinite run g(0)g(l)g(2)... is successful if and only ií {q E Q \ q = q{i) for infinitely many i } n F / 0. A finite run g(0)g(l)g(2)... q(n) is successful if and only if q(n) G F. Let us note, that the 1-weak Büchi automaton of [MaiOO], we have mentioned in Section 11.1, is the weak automaton of our definition using Büchi acceptance condition. As we consider the automaton on both finite and infinite runs, we call it simply a weak automaton. Remark 11.4. A run a of an automaton A = (Q, E, qo, R, F) is successful if and only if a |= GF(\JqeF q) where the atomic actions ranges over Q. An automaton A accepts a word u if there is a successful run of A over u. An automaton A = (Q,T,,qo,R,F) represents an LTL formula ip over an alphabet E if A accepts exactly the words over E that satisfy if, i.e. all models of

ip over E. Proof. The proof is based on induction on structure of if. We construct an automaton A^v = (Q, E, q, R, F) for every case of structure type of if, assuming that automata for its proper subformulae can be constructed. Case p: We construct a^p = ({Qi,Qo},^,Qi,R,F), where • R = {(qi, a, q0) \ a G E A a ^ p} U {(q0, a, q0) \ a G E}. • If e |= -ip then F = {q\, q0}; otherwise, F = {qo}. The automaton A^p can be depicted as follows. MQi ^p H(9o) )\=tt Case Xipi: Let A^Vl = (Q', E, q', R', F') and n = \Q'\. We construct ^(Xv-i) = (Q' U {qn}, S, qn, R, F' U {qn}), where R = {(qn, a, q') \ a G E} U R' and qn is fresh. The automaton A^(xvi) can be depicted as follows. \=tt A. "pi Case^iA^2: Let ^ = (Q>, E,,Z,q>,R>,F>),A^2 = (Q",E,q",R",F"),Q" = {q\Q>\+\Q"\-i, • • •> Q\Q>\h and n be equal to \Q'\ + |Q"|. We construct ^((pA^i)V(^pA^2)) = (Q' U Q" U Un}, E, p A Lp2). Here, A^v is the same as in the previous case, except that F = F'. Hence, the automaton A^^pAlfl^ w(^pa^2)) can ^e depicted as follows. D Lemma 11.6. Let Abe a wPRS and

j and p 3 r, • Const(A') = Const(A), and . R' = {p'X0 ^ (q\Q\-i,Po)XQ)} U {(qi,p)ti ^ (q',r)t2 | % G Q Apíi^ rt2 G R} U {{qi,p)t\ ^ (qj,r)t2) \ (qi,a,qj) G R" Aph A rt2 G R}. From the construction, it follows that there is a run violating if in A if and only if there is a run in A' that is successful for the component representing the formula. Due to Remark 11.4, the lemma holds. D Theorem 11.7. The model checking problem for wPRS and LTLdet is decidable. Proof. The theorem follows directly from Lemma 11.6 and decidability of the LTL(Fs, Gs) model checking problem for wPRS (see Corollary 10.25). D 11.4 SUMMARY 155 11.4 Summary It was easily deducible from [BH96] and [MaiOO], that the model checking problem for PA and the common fragment of CTL and LTL called LTL is decidable. In this chapter, we have shown that the LTL model checking problem (of both infinite runs and finite runs) is decidable also for wPRS. Our proof use some ideas of [MaiOO] and decidability of the model checking problem for LTL(FS, Gs) and wPRS (see Corollary 10.25). As LTL can express some reachability formulae e.g. (->halt) U halt, the LTLdet model checking problem is undecidable for all Turing powerful classes, i.e. sePA and all its superclasses. Therefore, the (un)decidability boundaries of the LTL model checking problem are established for the extended PRS-hierarchy, see Figure 11.1. 156 LTLUhl MODEL CHECKING sePRS und ecid able decidable v wPAD sePAN und ecid able decidable wPAN Figure 11.1: The extended PRS-hierarchy with (un)decidability boundaries of LTL model checking problem. Chapter 12 Conclusion and Future Work This thesis provides an overview of extensions of Process Rewrite System formalism (see Chapters 2-5). We construct a hierarchy of this formalisms with respect to the strong bisimulation equivalence. Within this hierarchy we examined various (un)decidability questions of interesting verification problems such as bisimulation equivalence (see Chapters 6 and 7) and model checking problems (see Chapters 8-11). On the one hand, we can say that all the borderlines related to all the discussed model checking problems are established for now. On the other hand, a lot of questions remain open in the area of equivalence checking, namely deciding bisimulation equivalence, for example strong bisimulation problem for fcBPP, wBPP, PA, fcPA, wPA, PAD, fcPAD, and wPAD (see Section 6.1) and weak bisimulation problem for BPA and BPP (see Section 7.5). Moreover, in this field there is a lot of important open problems that has not been objected in this thesis, for example strong/weak bisimilarity with finite state systems and strong/weak regularity as well as upper and lower complexity bounds of all the problems mentioned above. Bibliography [BAPM83] M. Ben-Ari, A. Pnueli, and Z. Manna. The temporal logic of branching time. Acta Information, 20(3):207-226,1983. [BCMSOl] O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In Handbook of Process Algebra, pages 545-623. Elsevier Science Publishers, 2001. [BCS95] O. Burkart, D. Caucal, and B. Steffen. An elementary bisimula-tion decision procedure for arbitrary context-free processes. In Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science (MFCS'95), volume 969 of Lec-tute Notes in Computer Science, pages 423-433. Springer-Verlag, 1995. [BCS96] O. Burkart, D. Caucal, and B. Steffen. Bisimulation collapse and the process taxonomy. In Proceedings of the 7th International Conference on Concurrency Theory (CONCUR'96), volume 1119 of Lectute Notes in Computer Science, pages 247-262. Springer-Verlag, 1996. [BE97] O. Burkart and J. Esparza. More infinite results. Electronic Notes in Theoretical Computer Science, 5,1997. [BEH95] A. Bouajjani, R. Echahed, and P. Habermehl. On the verification problem of nonregular properties for nonregular processes. In Proceedings of IEEE Symposium on Logic in Computer Science (LICS'95). IEEE Computer Society Press, 1995. [BEM97] A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR'97), volume 1243 of Lectute Notes in Computer Science, pages 135-150. Springer-Verlag, 1997. [BET03] A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. Interna- 160 BIBLIOGRAPHY tional Journal on Foundations of Computer Science, 14(4):551-582, 2003. [BH96] A. Bouajjani and P. Habermehl. Constrained properties, semi-linear systems, and petri nets. In Proceedings of the 7th International Conference on Concurrency Theory (CONCUR'96), volume 1119 of Lectute Notes in Computer Science, pages 481-497. Springer-Verlag, 1996. [BK85] J. A. Bergstra and J. W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37:77-121, 1985. [BKŘS06] L. Bozzelli, M. Křetínský, V. Řehák, and J. Strejček. On Decidability of LTL Model Checking for Process Rewrite Systems. In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, volume 4337 of Lectute Notes in Computer Science, pages 248-259. Springer-Verlag, 2006. [Boz05] L. Bozzelli. Model checking for process rewrite systems and a class of action-based regular properties. In Proceedings of VM-CAI'OS, volume 3385 of Lectute Notes in Computer Science, pages 282-297. Springer-Verlag, 2005. [BST06] A. Bouajjani, J. Strejček, and T. Touili. On Symbolic Verification of Weakly Extended PAD. In Preliminary Proceedings of the 13th International Workshop on Expressiveness in Concurrency EXPRESS'06, 2006. [BT03] A. Bouajjani and T. Touili. Reachability Analysis of Process Rewrite Systems. In Proceedings of Foundations of Software Technology and Theoretical Computer Science (FSTTCS'03), volume 2914 of Lectute Notes in Computer Science, pages 74-87. Springer-Verlag, 2003. [Büc64] J. R. Büchi. Regular canonical systems. Arch. Math. Logik u. Grundlagenforschung, 6:91-111,1964. [BW90] J. C. M. Baeten and W. P. Weijland. Process Algebra. Number 18 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990. [Cau92] D. Caucal. On the regular structure of prefix rewriting. Theoretical Computer Science, 106:61-86,1992. [CGP99] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999. BIBLIOGRAPHY 161 [CHM93] S. Christensen, Y. Hirshŕeld, and E Moller. Bisimulation is de-cidable for all basic parallel processes. In Proceedings of the 4th International Conference on Concurrency Theory (CONCUR'93), volume 715 of Lectute Notes in Computer Science, pages 143-157. Springer-Verlag, 1993. [DY83] D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198-208,1983. [EK95] J. Esparza and A. Kiehn. On the model checking problem for branching time logics and basic parallel processes. In CAV, volume 939 of Lectute Notes in Computer Science, pages 353-366. Springer-Verlag, 1995. [EPOO] J. Esparza and A. Podelski. Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In Proceedings of the 27th Symposium on Principles of Programming Languages (POPL'OO), pages 1-11. ACM press, 2000. [Esp94] J. Esparza. On the decidability of model checking for several mu-calculi and petri nets. In CAAP, volume 787 of Lectute Notes in Computer Science, pages 115-129. Springer-Verlag, 1994. [Esp97] J. Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 34(2):85-107,1997. [Esp02] J. Esparza. Grammars as processes. In Formal and Natural Computing, volume 2300 of Lectute Notes in Computer Science. Springer-Verlag, 2002. [EVW02] K. Etessami, M. Y. Vardi, and Th. Wilke. First-order logic with two variables and unary temporal logic. Information and Computation, 179(2):279-295, 2002. [GPSS80] D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Conference Record of the 7th Annual ACM Symposium on Principles of Programming Languages (POPĽ80), pages 163-173. ACM press, 1980. [Hab97] P. Habermehl. On the complexity of the linear-time /x-calculus for Petri nets. In Proceedings ofICATPN'97, volume 1248 of Lectute Notes in Computer Science, pages 102-116. Springer-Verlag, 1997. [Hir] Y Hirshfeld. Methods and tools for the verification of infinite state systems. Private communication. 162 BIBLIOGRAPHY [Hoa80] C. A. R. Hoare. Communicating Sequential Processes. In On the connstruction of programs - an advanced course, pages 229-254. Cambridge University Press, 1980. [HS05] H. Hüttel and J. Srba. Recursion vs. replication in simple cryptographic protocols. In Proceedings of SOFSEM 2005: Theory and Practice of Computer Science, volume 3381 of Lectute Notes in Computer Science, pages 178-187. Springer-Verlag, 2005. [HU79] J. E. Hopcroft and J. D. Ullman. Introduction To Automata Theory, Languages, And Computation. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1979. [Jan95a] P. Jančar. High Undecidability of Weak Bisimilarity for Petri Nets. In Proc. ofTAPSOFT, volume 915 of Lectute Notes in Computer Science, pages 349-363. Springer-Verlag, 1995. [Jan95b] P. Jančar. Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science, 148(2):281-301, 1995. [Jan03] P. Jančar. Strong bisimilarity on basic parallel processes is PSPACE-complete. In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS'03), pages 218-227. IEEE Computer Society Press, 2003. [JEM99] P. Jančar, J. Esparza, and F. Moller. Petri nets and regular processes. Journal of Computer and System Sciences, 59(3):476-503, 1999. [JKM01] P. Jančar, A. Kučera, and R. Mayr. Deciding bisimulation-like equivalences with finite-state processes. Theoretical Computer Science, 258:409-433,2001. [JM95] P. Jancar and F. Moller. Checking regular properties of petri nets. In Proceedings of the 6th International Conference on Concurrency Theory (CONCUR'95), volume 962 of Lectute Notes in Computer Science, pages 348-362. Springer-Verlag, 1995. [JS04] P. Jančar and J. Srba. Highly undecidable questions for process algebras. In Proceedings of the 3rd IFIP International Conference on Theoretical Computer Science (TCS'04), Exploring New Frontiers of Theoretical Informatics, pages 507-520. Kluwer Academic Publishers, 2004. [Kam68] J. A. W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, 1968. BIBLIOGRAPHY 163 [KM02] A. Kučera and R. Mayr. On the complexity of semantic equivalences for pushdown automata and BPA. In Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science (MFCS'02), volume 2420 of Lectute Notes in Computer Science, pages 433-445. Springer-Verlag, 2002. [KRS04a] M. Křetínský, V. Řehák, and J. Strejček. Extended process rewrite systems: Expressiveness and reachability. In Proceedings of 15th International Conference on Concurrency Theory (CON-CUR'04), volume 3170 of Lectute Notes in Computer Science, pages 355-370. Springer-Verlag, 2004. [KRS04b] M. Křetínský, V Řehák, and J. Strejček. On extensions of process rewrite systems: Rewrite systems with weak finite-state unit. In Proceedings of INFINITY 2003, the 5th International Workshop on Verification of Infinite-State Systems, a satellite workshop of CONCUR 2003, volume 98 of Electronic Notes in Theoretical Computer Science, pages 75-88. Elsevier Science Publishers, 2004. [KŘS05] M. Křetínský, V Řehák, and J. Strejček. Reachability of Hennessy-Milner properties for weakly extended PRS. In FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, volume 3821 of Lectute Notes in Computer Science, pages 213-224. Springer-Verlag, 2005. [KŘS06] M. Křetínský, V. Řehák, and J. Strejček. Refining the Undecid-ability Border of Weak Bisimilarity. In Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (IN-FINITY'05), volume 149 of Electronic Notes in Theoretical Computer Science, pages 17-36. Elsevier Science Publishers, 2006. [KS04] A. Kučera and Ph. Schnoebelen. A general approach to comparing infinite-state systems with their finite-state specifications. In CONCUR, volume 3170 of Lectute Notes in Computer Science, pages 371-386. Springer-Verlag, 2004. [Lip76] R. Lipton. The reachability problem is exponential-space hard. Technical Report 62, Department of Computer Science, Yale University, 1976. [LS98] D. Lugiez and Ph. Schnoebelen. The regular viewpoint on PA- processes. In Proceedings of the 9th International Conference on Concurrency Theory (CONCUR'98), volume 1466 of Lectute Notes in Computer Science, pages 50-66. Springer-Verlag, 1998. 164 BIBLIOGRAPHY [MaiOO] M. Maidl. The common fragment of CTL and LTL. In Proceedings of the 41th Annual Symposium on Foundations of Computer Science (FOCS'OO), pages 643-652,2000. [May81] E. W. Mayr. An algorithm for the general Petri net reachability problem. In Proceedings of 13th Symposium on Theory of Computing, pages 238-246. ACM press, 1981. [May84] E. W. Mayr. An algorithm for the general Petri net reachability problem. SIAM Journal on Computing, 13(3):441-460,1984. [May97a] R. Mayr. Combining Petri nets and PA-processes. In Proceedings of P ACS'97: International Symposium on Theoretical Aspects of Computer Software, volume 1281 of Lectute Notes in Computer Science, pages 547-561. Springer-Verlag, 1997. [May97b] R. Mayr. Process rewrite systems, in proceedings of EX-PRESS'97. Electronic Notes in Theoretical Computer Science, 7 (1997):185-205,1997. [May98] R. Mayr. Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD thesis, Technische Universität München, 1998. [MayOO] R. Mayr. Process rewrite systems. Information and Computation, 156(l):264-286,2000. [May05] R. Mayr. Weak bisimilarity and regularity of context-free processes is EXPTIME-hard. Theoretical Computer Science, 330(3):553-575,2005. [McM93] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA, USA, 1993. [Mil89] R. Milner. Communication and Concurrency. Prentice-Hall, 1989. [Min67] M. L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967. [Mol96] F. Moller. Infinite results. In Proceedings of the 7th International Conference on Concurrency Theory (CONCUR'96), volume 1119 of Lectute Notes in Computer Science, pages 195-216. Springer-Verlag, 1996. [Mol98] F. Moller. A taxonomy of infinite state processes. In Proceedings of International Symposium on Mathematical Foundations of Computer Science (MFCS'98), volume 18 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 1998. BIBLIOGRAPHY 165 [MR98] R. Mayr and M. Rusinowitch. Reachability is decidable for ground AC rewrite systems. In Proceedings ofINFINITY'98 workshop, 1998. [MS85] D. Müller and P. Schupp. The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science, 37:51-75,1985. [MSS92] D. Müller, A. Saoudi, and P. Schupp. Alternating automata, the weak monadic theory of trees and its complexity. Theoretical Computer Science, 97(2):233-244,1992. [Par81] D. Park. Concurrency and automata on infinite sequences. In Proceedings of 5th GTConference, volume 104 of Lectute Notes in Computer Science, pages 167-183. Springer-Verlag, 1981. [Pet81] J. L. Peterson. Petri Net Theory and the Modelling of Systems. Prentice-Hall, 1981. [Pnu77] A. Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS'77), pages 46-57,1977. [Rei85] W. Reisig. Petri Nets—An Introduction. Springer-Verlag, 1985. [Sén98] G. Sénizergues. Decidability of bisimulation equivalence for equational graphs of finite out-degree. In Proceedings of the 39th Annual Symposium on Foundations of Computer Science (FOCS'98), pages 120-129. IEEE Computer Society Press, 1998. [SR90] V A. Saraswat and M. Rinard. Concurrent constraint programming. In Proceedings of 17th Symposium on Principles of Programming Languages (POPĽ90), pages 232-245. ACM press, 1990. [Srb02a] J. Srba. Roadmap of infinite results. EATCS Bulletin, (78):163-175,2002. http: //www.brics . dk/~srba/roadmap/. [Srb02b] J. Srba. Strong bisimilarity and regularity of basic parallel processes is PSPACE-hard. In Proceedings of the 19th International Symposium on Theoretical Aspects of Computer Science (STACS'02), volume 2285 of Lectute Notes in Computer Science, pages 535-546. Springer-Verlag, 2002. [Srb02c] J. Srba. Strong bisimilarity and regularity of basic process algebra is PSPACE-hard. In Proceedings of 29th International Colloquium on Automata, Languages and Programming (ICALP'02), volume 2380 of Lectute Notes in Computer Science, pages 716-727. Springer-Verlag, 2002. 166 BIBLIOGRAPHY [Srb02d] J. Srba. Undecidability of weak bisimilarity for pushdown processes. In Proceedings of the 13th International Conference on Concurrency Theory (CONCUR'02), volume 2421 of Lectute Notes in Computer Science, pages 579-593. Springer-Verlag, 2002. [Srb03a] J. Srba. Complexity of weak bisimilarity and regularity for BPA and BPP. Mathematical Structures in Computer Science, 13:567-587,2003. [Srb03b] J. Srba. Undecidability of weak bisimilarity for PA-processes. In Proceedings of the 6th International Conference on Developments in Laguage Theory (DLT'02), volume 2450 of Lectute Notes in Computer Science, pages 197-208. Springer-Verlag, 2003. [Srb04] J. Srba. Roadmap of Infinite results, volume Vol 2: Formal Models and Semantics. World Scientific Publishing Co., 2004. [Sti96] C. Stirling. Modal and temporal logics for processes. In F. Moller and G. M. Birtwistle, editors, Banff Higher Order Workshop 1995, volume 1043 of Lectute Notes in Computer Science, pages 149-237. Springer-Verlag, 1996. [Str02] J. Strejček. Rewrite systems with constraints, in proceedings of EXPRESS'01. Electronic Notes in Theoretical Computer Science, 52, 2002. [Str04] J. Strejček. Linear Temporal Logic: Expressiveness and Model Checking. PhD thesis, Faculty of Informatics, Masaryk University in Brno, 2004. [vG93] R. J. van Glabbeek. The linear time - branching time spectrum II. In Proceedings of the 4th International Conference on Concurrency Theory (CONCUR'93), volume 715 of Lectute Notes in Computer Science, pages 66-81. Springer-Verlag, 1993.