Graph transformation planning with time and concurrency / vorgelegt von Steffen Ziegert, M.Sc.

Graph Transformation Planning with Time and Concurrency Dissertation zur Erlangung des akademischen Grades eines Doktors der Naturwissenschaften an der Fakultät für Elektrotechnik, Informatik und Mathematik der Universität Paderborn vorgelegt von Steffen Ziegert, M.Sc. Paderborn 2016 iii Abstract The increasing complexity of technical systems inspires software and systems engineering scientists to improve the state of the art in designing such systems. Among these improvements is the integration of cognitive functions into approaches to model-driven software development. Such cognitive functions enable an autonomous operation of the system, e.g., by planning reconfiguration behavior affecting the software architecture of the system. In this context, this thesis is concerned with the automated generation of reconfiguration plans. By providing a formal framework for the rule-based modification of graphs or graph-like structures, graph transformation systems enable to model the dynamics of structures. As a consequence, they are particularly convenient for modeling reconfiguration behavior of software architectures. However, graph transformation systems have only rarely been employed as system models for planning techniques. Motivated by different requirements arising from two fundamentally different application examples, two approaches for graph transformation planning have been developed in this thesis. The first approach preserves the expressiveness of graph transformation systems by directly working on a graph transformation system’s state space. As a result, it can handle system models with an infinite state space. It employs a domain-specific heuristic function that uses the solution length of a relaxed planning problem as heuristic estimate. Taking both the structure of graphs and applicable graph transformations into account, this is a considerable improvement over related work. The second approach puts its focus on timing aspects and concurrency. It comes with a new formalism for the specification of durative graph transformations. This formalism ensures that multiple durative graph transformations with conflicting behavior cannot be executed concurrently. Furthermore, it enables the explicit, rule-based specification of requirements regarding their concurrent and urgent execution. By being based on timed graph transformation systems, it also allows to employ available verification procedures. System models that have been designed in this formalism can be translated into planning domains, for which problem instances can be solved by employing off-the-shelf planning systems. Evaluation results give insight on how to decide between different translation variants and convoy an idea how certain aspects of planning domains influence planning performance. iv Zusammenfassung Die zunehmende Komplexität von technischen Systemen motiviert Forscher im Software und Systems Engineering den Stand der Technik der Entwicklung solcher Systeme zu verbessern. Zu diesen Verbesserungen gehört die Integration kognitiver Funktionen in Ansätze der modellgetriebenen Softwareentwicklung. Solche kognitive Funktionen ermöglichen einen autonomen Betrieb des Systems, z.B. durch eine Planung von Rekonfigurationen, die die Softwarearchitektur des Systems beeinflussen. In diesem Zusammenhang beschäftigt sich diese Arbeit mit der automatischen Erstellung von Plänen solcher Rekonfigurationen. Indem sie ein formales Framework für die regelbasierte Modifikation von Graphen und Graph-ähnlichen Strukturen zur Verfügung stellen, ermöglichen es Graphtransformationssysteme, die Dynamik von Strukturen zu modellieren. Sie sind damit besonders zur Modellierung von Rekonfigurationen einer Softwarearchitektur geeignet. Bisher wurden Graphtransformationssysteme jedoch nur selten als Modelle für Planungsverfahren eingesetzt. Motiviert durch die unterschiedlichen Anforderungen zweier grundverschiedener Anwendungsbeispiele, wurden in dieser Arbeit zwei Verfahren zur Planung mit Graphtransformationen entwickelt. Das erste Verfahren erhält die Ausdruckskraft von Graphtransformationssystemen, indem es direkt auf dem Zustandsraum eines Graphtransformationssystems arbeitet. Aus diesem Grund kann es mit Modellen umgehen, die einen unendlichen Zustandsraum aufspannen. Es verwendet eine domänenunabhängige Heuristik, die die Länge der Lösung eines relaxierten Planungsproblems als Schätzwert liefert. Sie berücksichtigt sowohl die Struktur des Graphen als auch die anwendbaren Graphtransformationen, was eine deutliche Verbesserung gegenüber verwandten Arbeiten darstellt. Das zweite Verfahren legt seinen Fokus auf Zeitaspekte und Nebenläufigkeit. Es bringt einen neuen Formalismus zur Spezifikation von zeitkonsumierenden Graphtransformationen mit sich. Dieser Formalismus stellt sicher, dass mehrere zueinander im Konflikt stehende zeitkonsumierende Graphtransformationen nicht nebenläufig ausgeführt werden können. Des Weiteren ermöglicht er die explizite, regelbasierte Spezifikation von Anforderungen bezüglich ihrer nebenläufigen und eiligen Ausführung. Indem er auf zeitbehafteten Graphtransformationen aufsetzt, ermöglicht er außerdem die Verwendung bereits verfügbarer Verifikationsverfahren. In diesem Formalismus entwickelte Modelle können in Planungsdomänen übersetzt werden, dessen Probleminstanzen mit Standard- Planungssystemen gelöst werden können. Auswertungsergebnisse helfen zwischen unterschiedlichen Varianten dieser Übersetzung zu entscheiden und vermitteln eine Idee, inwiefern die Performanz der Planung durch verschiedene Aspekte der Planungsdomäne beeinflusst wird. v Acknowledgments First of all, I would like to thank my PhD advisor Prof. Dr. Heike Wehrheim for her support and guidance during these past five years and the opportunity to write this PhD thesis. I would further like to thank Prof. Dr. Wilhelm Schäfer for this time and interest in the evalation of my thesis and Dr. Theo Lettmann, Prof. Dr. Leena Suhl, and Prof. Dr. Christian Plessl for serving as thesis comittee members. Special thanks go to Dr. Dominik Steenken, Dr. Claudia Priesterjahn, Dr. Christian Heinzemann, Oliver Sudmann, Tobias Meyer, Christoph Rasche, and Prof. Dr. Matthias Tichy for the productive and enjoyable collaboration within the Collaborative Research Centre 614 and overlapping research interests. I would also like to thank the (former) members of our research group Dr. Thomas Ruhroth, Dr. Nils Timm, Dr. Galina Besova, Daniel Wonisch, Sven Walther, Alexander Schremmer, Oleg Travkin, Tobias Isenberg, Marie-Christine Jakobs, Manuel Töws, Julia Krämer, and Elisabeth Schlatt for providing a warm and inspiring atmosphere. A similar contribution has been made by various colleagues from across the floor. Thank you for making coffee breaks more enjoyable! Additionally, I would like to thank my student assistants Shayan Ahmadian and Johannes Geismann for supporting me in developing parts of the thesis implementation and my thesis advisees Marcel Friedrich, Thomas Hauck, and Johannes Heil for interesting discussions in research themes related to this PhD thesis. Finally, I would like to thank my wife and parents for their support and patience during these years of research (and all those years before) and my brother for sparking my interest in computer science in the first place. Contents List of Figures xi List of Tables xv List of Algorithms xvii List of Listings xix 1 Introduction 1 1.1 AutomatedPlanning............................. 3 1.2 Rule-Based Modification of Graphs . . . . . . . . . . . . . . . . . . . . 4 1.3 Research Tasks and Contributions . . . . . . . . . . . . . . . . . . . . . 5 1.4 ApplicationExamples ............................ 8 1.5 ThesisOutline................................. 11 2 Background on Graph Transformations 13 2.1 Graphs, Graph Morphisms, and Pushouts . . . . . . . . . . . . . . . . . 15 2.2 Double Pushout Approach . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.3 Single Pushout Approach . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.4 NACs, Types, and Visual Representation . . . . . . . . . . . . . . . . . 21 2.5 Parallel and Sequential Independence . . . . . . . . . . . . . . . . . . . 23 3 Background on AI Planning 27 3.1 PDDLFundamentals............................. 28 3.2 NumericExpressions............................. 31 3.3 DurativeActions ............................... 32 3.4 RequiredConcurrency............................ 33 4 Planning with Graph Transformations 35 4.1 ProblemStatement .............................. 37 vii viii CONTENTS 4.2 Application Example: Reconfiguration of ECUs . . . . . . . . . . . . . 38 4.3 Relaxed Planning Heuristic . . . . . . . . . . . . . . . . . . . . . . . . . 40 4.3.1 Abstract State Sequences . . . . . . . . . . . . . . . . . . . . . . 40 4.3.2 Rule Application Labels . . . . . . . . . . . . . . . . . . . . . . . 44 4.3.3 ProgramCode ............................ 46 4.4 Evaluation................................... 50 4.5 RelatedWork ................................. 56 4.6 Discussion................................... 59 5 Durative Graph Transformation Systems 65 5.1 Application Example: RailCab System . . . . . . . . . . . . . . . . . . . 67 5.2 Durative Graph Transformation Rules . . . . . . . . . . . . . . . . . . . 68 5.2.1 Syntax ................................. 72 5.2.2 Timed Graphs and Clock Instances . . . . . . . . . . . . . . . . 73 5.2.3 Locking Edges and Application Indicators . . . . . . . . . . . . 76 5.2.4 Timed Graph Transformation Rules . . . . . . . . . . . . . . . . 79 5.2.5 Clock Instance and Invariant Rules . . . . . . . . . . . . . . . . 84 5.2.6 Operational Semantics . . . . . . . . . . . . . . . . . . . . . . . . 87 5.3 Properties of Durative Graph Transformation Rules . . . . . . . . . . . 90 5.3.1 Correspondence of a Durative Graph Transformation . . . . . . 90 5.3.2 Rule Termination and Interleaving Transition Sequences . . . . 92 5.4 Support for Negative Application Conditions . . . . . . . . . . . . . . . 102 5.5 ConcurrencyRules ..............................107 5.5.1 Syntax .................................108 5.5.2 Semantics ...............................114 5.6 UrgencyRules.................................120 5.6.1 Syntax .................................122 5.6.2 Semantics ...............................124 5.7 RelatedWork .................................131 5.8 Discussion...................................134 6 Temporal PDDL-Based Planning for Durative Graph Transformation Systems 139 6.1 ProblemStatement ..............................141 6.2 Application Example: RailCab System (Emphasis on NACs) . . . . . . 143 6.3 TranslationScheme..............................146 6.3.1 TypeGraph ..............................148 6.3.2 Durative Graph Transformation Rules . . . . . . . . . . . . . . . 149 6.3.3 ForbiddenPairs............................151 6.3.4 DanglingEdges............................154 6.3.5 Locking Functionality . . . . . . . . . . . . . . . . . . . . . . . . 155 6.3.6 Locks in Durative Rules . . . . . . . . . . . . . . . . . . . . . . . 156 6.3.7 Concurrency Rules . . . . . . . . . . . . . . . . . . . . . . . . . . 161 6.3.8 UrgencyRules ............................164 6.4 Prototype and Translation Workflow . . . . . . . . . . . . . . . . . . . . 167 CONTENTS ix 6.5 Evaluation of Translation Variants . . . . . . . . . . . . . . . . . . . . . 168 6.6 Evaluation of Concurrency and Urgency Rules . . . . . . . . . . . . . . 171 6.7 RelatedWork .................................177 6.8 Discussion...................................178 7 Conclusion and Future Work 181 Bibliography 185 List of Algorithms 4.1 RelaxedNACmatching ............................. 47 4.2 Collecting rule application labels from an LHS match . . . . . . . . . . . . 48 4.3 Heuristic function yielding the length of a relaxed plan . . . . . . . . . . . 49 xvii List of Listings 3.1 An example domain desciption in PDDL [FL03] . . . . . . . . . . . . . . . 29 3.2 A problem description to the domain of Listing 3.1 [FL03] . . . . . . . . . 30 3.3 A domain description with numeric expressions [FL03] . . . . . . . . . . . 31 6.1 Excerpt of a plan for 4 RailCabs . . . . . . . . . . . . . . . . . . . . . . . . . 146 6.2 Generated declaration of types, predicates, and functions . . . . . . . . . 149 6.3 Generated durative action for the durative rule joinConvoy ........150 6.4 Generated negative existential quantification for a forbidden pair . . . . . 152 6.5 Generated declarations for the counting functionality . . . . . . . . . . . . 153 6.6 Generated numeric facts and assignments for forbidden pairs . . . . . . . 153 6.7 Generated universal quantification for deleting dangling edges (in the SPO variant with quantifications) . . . . . . . . . . . . . . . . . . . . . . . . 154 6.8 Generated durative action for deleting dangling edges (in the SPO variant withcountingfunctions).............................155 6.9 Generated declarations for the locking functionality . . . . . . . . . . . . . 156 6.10 Generated locks to support (required) nodes . . . . . . . . . . . . . . . . . 157 6.11 Generated locks to support required and forbidden edges . . . . . . . . . 158 6.12 Generated adjacency locks to support forbidden pairs . . . . . . . . . . . 160 6.13 Generated declarations to support concurrency rules . . . . . . . . . . . . 162 6.14 Generated concurrency demand in the rule changePublication ......163 6.15 Generated concurrency satisfaction in the rule moveRailCab ........163 6.16 Generated declarations to support urgency rules . . . . . . . . . . . . . . . 165 6.17 Clip action to support urgency rule immediatelyMoveRailCab .......166 6.18 Generated urgency demand in the rule accelerateRailCab ........166 6.19 Generated urgency satisfaction in the rule brakeRailCab ..........166 xix 1 Introduction In today’s economy, more and more technical systems contain large amounts of software. The increasing complexity of these systems gave rise to the use of modeling languages, which allow to create a model of the system that is to be developed. Such a model usually abstracts details of the system away or allows to hide them in different views, thus making the model easier to understand. However, the opportunities of employing modeling languages during the development of software systems go far beyond that of abstractly representing systems for easier discussion and documentation. Model-Driven Software Development (MDSD) [SV06] tries to benefit from the existence of models by considering them as first-class artifacts during the development of software systems. The aim of MDSD is to enable the generation of code from models, e.g., via model transformation techniques [OMG11], making a lengthy and error-prone direct implementation unnecessary. A related goal is to enable the analysis of the same models, e.g., to verify their correctness or to ensure a certain level of quality. The benefits of a well-functioning MDSD approach are obvious: software systems are much easier to develop and errors can be found earlier in the development process. For an MDSD approach to function properly, its system models need to have a formal foundation, i.e., a mathematical basis that unambiguously defines a model’s meaning. Development techniques in the area of software engineering and hardware design that provide such a formal foundation are called formal methods. Examples for formal methods include process calculi, like Hoare’s Communicating Sequential Processes (CSP) [Hoa78] and Milner’s Calculus of Communicating Systems (CCS) [Mil80], formal specification languages, like the Z notation [Spi92; ISO02] and Alloy [Jac06], and automata theory. MDSD approaches, like MechatronicUML [Bec+12], are likely to combine multiple domain-specific modeling languages, each specialized to a certain kind of modeling task. Examples for such modeling tasks include modeling the structural 1 2CHAPTER 1. INTRODUCTION relationship of software components, communication behavior between different components, and reconfiguration behavior. The latter states how the structural relationship of software components may change over time. Because reconfiguration impacts the software architecture of a system, it is usually treated separately from other behavior. The increasing complexity of technical systems also inspired software and systems engineering scientists to look into different fields, like control theory, optimization, and artificial intelligence, to improve the state of the art in designing those systems, cf. [GRS14]. Among these improvements is the integration of cognitive functions into MDSD approaches. This enables subsystems of the system under consideration to operate autonomously and thus ensures that they require only low maintenance. These cognitive functions allow to perceive situations and add some kind of partial intelligence to the technical system. To enable a technical system to operate autonomously, one has to integrate a means of making decisions into this system. For each decision, there may be a large set of alternatives. Selecting which alternative to put into practice should not be done in isolation from other decisions. Systems operating autonomously usually have goals that are supposed to be reached during operation, like optimizing the consumption of time or resources, or achieving user-specified objectives. These goals have to be taken into account when deciding which alternatives to realize. However, recognizing those alternatives that are likely to help in achieving the goal can be a complex task. If these decisions were to be made by humans, the response-time requirements of many technical systems would not be met. As a consequence, the system needs a software component that plans which alternatives to take. Executing some of the chosen alternatives may involve reconfigurations to the system’s software architecture, such as the creation and deletion of software component instances or communication links between them. Systems that autonomously decide when and how to perform these reconfigurations, are said to have a selforganizing [GMK02] or self-managing [Bra+04] architecture. Multiple architectural models have been proposed for the development of such systems, e.g., the Operator- Controller Module (OCM) [HOG04], which was developed as part of the Collaborative Research Centre “Self-Optimizing Concepts and Structures in Mechanical Engineering” (CRC 614), or Kramer and Magee’s reference model for self-managing systems [KM07]. A schematic representation of the OCM is given in Figure 1.1. Both architectural models consist of three layers. The bottom layer, called controller (in the OCM) or component control (in the reference model), accomplishes the most basic tasks of the system. It essentially provides the implementation of primitive features related to sensors and actuators. The middle layer, called reflective operator (in the OCM) or change management (in the reference model), has the capability to modify the system’s architecture, e.g., it selects operating parameters for the bottom layer or executes software architecture reconfigurations. The top layer, called cognitive operator (in the OCM) or goal management (in the reference model), accomplishes time-consuming tasks, like the computation of a plan that determines which decision alternatives to realize. In a system with a self-managing architecture, 1.1. AUTOMATED PLANNING 3 Action Level Planning Level Monitoring Sequencer Reflective Operator Controller Operator-Controller-Module (OCM) ... Configuration- Control Emergency Soft Real Time Hard Real Time Model-based Self-Optimiazation Behavior-based Self-Optimization Cognitive Information Processing Cognitive Operator Cognitive Loop Reflective Loop Reflective Information Processing Motor Information Processing Configurations Controlled System Motor Loop A C B C B A Figure 1.1: Structure of the Operator-Controller Module such a plan states which architecture reconfigurations to perform and when. This thesis is specifically concerned with this last layer of those architectural models, i.e., with the automated generation of reconfiguration plans. 1.1 Automated Planning Automated planning is a discipline in the area of artificial intelligence, coming along in many different variants. In most of these variants, some kind of agent has to choose among some set of activities which one to perform. Usually, there is a notion 4CHAPTER 1. INTRODUCTION of a state or configuration, and each activity defines a transition between two such states. States and state transitions can be represented in almost any kind of form. Independently of the manner chosen to represent system states, a planning task always has some kind of initial state and a goal specification. The goal specification determines whether a state of the state space is a valid end state for the purpose of the planning task. If a planning system finds such an end state in the state space originating from the initial state of a planning task, then the path from the initial state to the end state constitutes a valid plan. Usually, there is also some kind of objective involved, e.g., state changes can have costs, which are to be minimized. In the most simple case, these costs are distributed uniformly, i.e., the objective is to reach the goal in as few steps as possible. If time is of the essence, the objective is usually to reach the goal in as little time as possible. A conventional representation for actions and states of planning problems, which is used throughout the AI planning research community, is based on (quantifier-free) predicate calculus. In this representation, an action is schematically defined via a set of atomic formulas that are required to hold, a set of atomic formulas that are asserted as true, and a set of atomic formulas that are asserted as false. This classical formalism is called STRIPS, named after a planning system developed by Fikes and Nilsson [FN71] in 1971. It is still in use today within the planning research community and has been integrated into a common language, called the Planning Domain Definition Language (PDDL), by McDermott and the AIPS-98 Planning Competition Committee [MA98] in 1998. PDDL has since been extended by several other contributors. The most relevant extensions with regard to this thesis are typing, which allows to employ a type hierarchy for objects appearing as terms in atomic formulas, and durative actions [FL03], which introduce a notion of time and concurrent execution into PDDL. Further extensions that are made use of in this thesis include the support for numeric formulas and quantification. Naturally, the application of planning techniques is not restricted to such classical representations. Planning has also been applied to graphical models such as Petri nets [Pet62], e.g., for solving assembly problems in manufacturing [Zha89; McC94], and in more recent times, to graph transformation systems [Ehr+06], e.g., for solving reconfiguration problems in the context of cyber-physical systems [EW11]. Both Petri nets and graph transformation systems are formal modeling languages with rigorous mathematical definitions and execution semantics. Petri nets are very well suited for modeling the concurrent behavior of distributed systems, and graph transformation systems enable to model the dynamics of structures by providing a formal framework for a rule-based modification of graphs or graph-like structures. The latter is particularly convenient for modeling reconfiguration behavior of software architectures. 1.2 Rule-Based Modification of Graphs In graph transformation systems, the modification of graphs is specified via graph transformation rules. Each graph transformation rule defines a condition that has to 1.3. RESEARCH TASKS AND CONTRIBUTIONS 5 be fulfilled by a graph so that the rule may be applied to this graph. If the condition is fulfilled, the rule gives one or more options how the graph may be transformed into a new graph. Since graphs provide an intuitive way to describe complex concepts and relations, graph transformations offer a wide range of application areas. Research on graph transformation started in the late 1960s in the fields of pattern recognition and compiler construction. Since then, graph transformations have been applied in software engineering, database design, modeling of concurrent systems, logical programming, model transformation, and many other areas. Their strength lies in their ability to model the dynamics of graphical structures. For this reason, graph transformations have been considered a new paradigm for developing software, especially if this software is of complex structure. A lot of structural information appears in the fields of software development and visual modeling. In object-oriented design, for example, there is structural information in the relationship between different classes and objects. Computer networks and component-based software systems are also built using a large amount of structural information. All this structural information can be expressed via graphs, and their evolution can be expressed via graph transformations. Due to its ability to specify how structures evolve over time, graph transformations have been used for the specification of software architecture reconfiguration, e.g., by Wermelinger and Fiadeiro [WF99; WF02], by Taentzer at al. [TGM00], or by Le Métayer [Le 98]. Since graph transformations have a formal foundation, they have also been used for verification. A prominent example is the tool set GROOVE [Ren04], which provides explicit CTL and LTL model checking for graph transformation systems [KR06; Ren08]. There are also approaches to the more specific case of verifying software architecture reconfiguration, e.g., a symbolic invariant checking technique by Becker et al. [Bec+06], which allows to prove the absence of forbidden graph patterns, and a compositional verification approach by Eckardt et al. [Eck+13], which includes the verification of timed properties. However, graph transformation systems have only rarely been employed as system models for planning techniques. 1.3 Research Tasks and Contributions The main purpose of this thesis is to design planning techniques based on graph transformations. The use of graph transformations renders these planning techniques suitable for software architecture reconfiguration and allows for an integration with MDSD approaches. Depending on the application scenarios of interest, e.g., whether or not they involve timing aspects and concurrent behavior, there are different requirements for such graph transformation planning systems. In general, reconfigurations of a system’s software architecture take time. If multiple such temporal reconfigurations are non-conflicting, they can probably be carried out in parallel. Requiring a strictly sequential execution of reconfigurations might even be counterintuitive in certain application domains, e.g., where reconfigurations 2 Background on Graph Transformations In graph grammars and graph transformation systems, the modification of graphs is specified via graph transformation rules 1 . Each rule consists of a pair of graphs, called left-hand side (LHS) and right-hand side (RHS), which schematically define how a graph may be transformed into a new graph. Applying a graph transformation rule to a graph can be seen as replacing a subgraph corresponding to the rule’s LHS with a copy of its RHS. More precisely, elements that are specified in both LHS and RHS are preserved by the rule application, elements specified only in the LHS are deleted, and elements specified only in the RHS are created. When a graph transformation rule is applied to a graph, this graph is called host graph to not confuse it with the LHS and RHS of the rule, which are also graphs. Naturally, the possibility of applying a graph transformation rule to a host graph underlies the condition that a subgraph corresponding to the rule’s LHS can be found. Furthermore, it is also possible that multiple matching subgraphs exist in a host graph. In such a case, multiple rule applications of the same rule can be performed. These rule applications are not necessarily independent. It might be the case that a choice has to be made at which match to transform the host graph, e.g., when different matches overlap and each their respective graph transformation modifies element contained in the other match. A set of graph transformation rules together with an initial graph spans a transition system. In this transition system, graphs are represented as states and graph transformations as transitions between states. It is important to realize that the nondeterminism indicated by multiple outgoing transitions of a state has two sources: multiple rules may be applicable to a graph and they may potentially be applied at multiple matches. There exist various approaches to realize graph transformations. They are broadly classified into connecting approaches and gluing approaches. The main difference of these approaches is how they attach a new replacement subgraph to the remainder 1A graph transformation rule is also known as graph production, cf. [Cor+97; Ehr+06]. 13 14 CHAPTER 2. BACKGROUND ON GRAPH TRANSFORMATIONS of the host graph. Connecting approaches introduce new edges to connect the new subgraph to the remainder graph. Gluing approaches identify or “glue together” certain elements of the new subgraph with elements of the remainder graph. In the node replacement approach [JR80; ER97], a graph transformation replaces a single node in a graph with a new subgraph. This subgraph is connected with new edges to the remainder graph according to an embedding relation. There are various ways to define such an embedding relation. Consequently, there are several extensions and variations of this approach. All of these variations belong to the connecting approaches. In the hyperedge replacement approach [Fed71; Pav72; DKH97], a hyperedge is replaced by a new hypergraph. This approach does not require an embedding relation. The new hypergraph is glued to the remainder hypergraph by identifying designated attachment nodes with nodes of the remainder hypergraph. This approach belongs to the group of gluing approaches. There are two notable algebraic approaches, the double pushout (DPO), which was invented by Ehrig et al. [EPS73; Cor+97; Ehr+06] and the single pushout (SPO) approach, which was invented by Löwe et al. [Löw93; Ehr+97]. Both approaches are based on category theory and the categorical term of a pushout. In DPO, a transformation is formalized via two pushouts in the category of graphs and (total) graph morphisms. One of the pushouts realizes the deletion of elements and the other one realizes their addition. In SPO, only a single pushout is used, which is a pushout in the category of graphs and partial graph morphisms. Both approaches belong to the gluing approaches. The two algebraic approaches differ in how they handle certain situations. In DPO, the application of a rule is not allowed at a match if it causes one or more dangling edges. The DPO approach also requires that no element in the host graph may have more than one preimage under the match if any of these preimages is to be deleted. Therefore, a transformation deletes exactly as many elements as specified in the rule. The SPO approach has no such restrictions on the applicability of rules. Dangling edges are simply deleted, and situations where an element in the host graph has multiple preimages under the match, one of them specified to be deleted and the other one to be preserved, are also resolved by deleting the element in question. The algebraic approaches also have alternative set-theoretic presentations, which are commonly seen in tutorial introductions, e.g. [EKL91; BH02], and include explicit constructions of successor graphs. As for practical matters, their workings and outcome are the same. The successor graphs of the set-theoretic and those of the algebraic versions are equivalent up to isomorphism. We adhere to the algebraic versions, which are deemed more suitable for proofs than the explicit constructions, cf. [Cor+97, p. 187]. Other well-known approaches to graph transformation are Courcelle’s monadic second-order logic of graphs [Cou90; Cou97], which uses logical formulas to specify graph properties and graph transformations, the theory of 2-structures by Ehrenfeucht el al. [EHR97], which is a relational framework for the decomposition and transfor- 2.1. GRAPHS, GRAPH MORPHISMS, AND PUSHOUTS 15 mation of graphs, as well as approaches to programmed graph replacement [Sch97], which employ control programs to steer the application of graph transformation rules. The formal semantics of timed and durative graph transformation systems, which is provided in Chapter 5, follows the SPO approach. However, there is no conceptual restriction to the SPO approach; the presented concepts work perfectly well in a DPO context. This is why the translation of durative graph transformation system models into PDDL allows to choose whether to comply with the DPO or SPO semantics. The next sections present the fundamentals of these two approaches. Section 2.1 lays the algebraic foundation for both approaches. It introduces the notions of graphs, graph morphisms, and pushouts. Sections 2.2 and 2.3 explain the workings of graph transformations in the DPO and SPO approach, respectively. Section 2.4 introduces negative application conditions and illustrates the graphical representation used for graph transformation rules in this thesis. The last section, Section 2.5, introduces the notions of parallel and sequential independence of graph transformations. These notions play a vital role in proving properties of the semantics of durative graph transformation systems. The definitions provided in this chapter are loosely based on the monograph Fundamentals of Algebraic Graph Transformation [Ehr+06] and the first volume of the Handbook of Graph Grammars and Computation by Graph Transformation, in particular the chapters on the DPO approach [Cor+97] and the SPO approach [Ehr+97]. The DPO approach primarily follows the formalization provided in [Ehr+06]; the SPO approach follows that provided in [Ehr+97]. The notions of parallel and sequential independence follow that of Habel et al. [HHT96]. We also provide less strict variants of parallel and sequential independence that take advantage of the existence of isomorphic matches. Although the idea of graph rewriting modulo isomorphism is not new, cf. [Plu05], we did not find definitions for parallel and sequential independence modulo isomorphism in related work. 2.1 Graphs, Graph Morphisms, and Pushouts A graph is a structure that represents a set of objects along with relations between them. Here, we consider only directed graphs. Undirected graphs can be simulated by adding both directed edges for each undirected edge. Definition 2.1.1 (Graph) . A(directed) graph G= (VG , EG , srcG , tgtG) consists of a set of nodes VG , a set of edges EG , and source and target functions srcG , tgtG:EG→VG . This definition of a graph allows parallel edges, i.e., edges whose pair of source and target node is identical to the pair of source and target node of another edge. Our semantics of durative graph transformations makes use of parallel edges. Each read access to a node or edge is realized as another (possibly parallel) edge. Multiple concurrent read accesses to the same node or edge thus result in multiple parallel edges. Another common definition of graphs defines the set of edges such that 16 CHAPTER 2. BACKGROUND ON GRAPH TRANSFORMATIONS E⊆V×V . Such a definition does not allow parallel edges. However, it can be used to simulate graphs that do support parallel edges, cf. [Bon+07]. Relations between graphs can be expressed through graph morphisms. A graph morphism is a mapping of nodes and edges of one graph to nodes and edges of another graph such that the source and target nodes of edges are preserved. Such morphisms are used in graph transformation rules to define which nodes and edges are created, deleted, or preserved when the rule is applied to a graph. Definition 2.1.2 (Graph morphism, partial graph morphism) . Agraph morphism f:G→H between two graphs is a pair of mappings f= (fE , fV) with fE:EG→ EH and fV:VG→VH that commutes with the source and target functions, i.e., fV◦srcG=srcH◦fE and fV◦tgtG=tgtH◦fE . A graph morphism f= (fE , fV) is called injective if fE and fV are injective and called isomorphic if fE and fV are bijective. Asubgraph S of G , written S⊆G or S,→G , is a graph with VS⊆VG and ES⊆EG such that srcS=srcG|ES and tgtS=tgtG|ES . A partial graph morphism g from G to H is a (total) graph morphism from a subgraph of G to H . This subgraph is called the restricted domain of g , written dom(g) . The range of a graph morphism g0:G→H , written ran(g0) , is a subgraph S0 of H where VS0 is the image set of g0 V and ES0is the image set of g0 E. The application of graph transformation rules is based on the concept of “gluing” graphs together. Two different graphs sharing a common subgraph can be glued together by adding the uncommon nodes and edges of both graphs to the common subgraph. This is formalized by the categorical notion of a pushout. Definition 2.1.3 (Pushout) . Let f:A→B and g:A→C be two morphisms in a category C . A pushout (D , f0 , g0) over f and g is defined by a pushout object D and morphisms f0:C→Dand g0:B→Dsuch that •g0◦f=f0◦gand (commutativity) • for all objects X and morphisms h:B→X and k:C→X with h◦f=k◦g , there is a unique morphism x:D→Xsuch that x◦g0=hand x◦f0=k. (universal property) AB CD f g f0 g0 X x h k = = = 2.2. DOUBLE PUSHOUT APPROACH 17 Here, A is the common subgraph. The pushout object D is the result of gluing B and C via A , f , and g . The commutativity ensures that all elements of B and C that have a common preimage in A are glued together in D . The universal property ensures that • elements of B and C that do not have a common preimage in A are not glued together in Dand •Ddoes not contain elements that neither exist in Bnor C. If elements of B and C were glued together in D , then there would exist a graph X for which no morphism x:D→X satisfies x◦g0=h and x◦f0=k , because x had to map the glued element simultaneously to different elements in X for x◦g0=h and x◦f0=k to hold. If D did contain elements that exist neither in B nor C , there would also exist such a graph, e.g., a subgraph of D that does not contain these elements. 2.2 Double Pushout Approach In the double pushout approach, a graph transformation rule connects its LHS and RHS via a so-called gluing graph 2 , which is a common subgraph of the LHS and RHS. The gluing graph represents those nodes and edges that are preserved during the application of the rule. To identify these nodes and edges in the LHS and RHS, two total graph morphisms are used. Elements of the LHS and RHS that are outside of the range of these morphisms represent those elements that are being deleted and created by the application of the rule, respectively. Definition 2.2.1 (Graph transformation rule (DPO)) . Agraph transformation rule p= (L , K , R , l , r) consists of three graphs L , K , and R , called left-hand side (LHS),gluing graph, and right-hand side (RHS), respectively, and two injective graph morphisms l:K→Land r:K→R. The semantics of the application of a rule is given by two pushouts in Graph , the category of graphs and (total) graph morphisms, cf. [Ehr+06]. The first pushout handles the deletion of nodes and edges, the second pushout their addition. However, whether or not the first pushout can be constructed depends on the host graph and the match of the LHS to the host graph. Definition 2.2.2 (Applicability of a rule (DPO)) . A graph transformation rule p= (L , K , R , l , r) is applicable at a match m:L→G , if and only if a context graph D can be constructed such that there exists a pushout (G , l∗ , m) over l:K→L and k:K→D in Graph. 2The gluing graph of a graph transformation rule is also known as interface, cf. [Cor+97]. 18 CHAPTER 2. BACKGROUND ON GRAPH TRANSFORMATIONS K R D r k L G l l∗ m(PO) The context graph is unique up to isomorphism if it exists. However, if the deletion of nodes results in the existence of dangling edges, the context graph cannot be constructed. This is because the definition of a graph does not allow any dangling edges. The pushout can also not be constructed if the images of elements in L have been merged by m into the same element in G and at least one of these elements is not going to be preserved. In such a case the universal property of the pushout does not hold. Unfortunately, this definition makes it rather difficult to see whether a graph transformation rule is applicable at a given match. Fortunately, there exists an equivalent notion of a rule’s applicability, called the gluing condition, cf. [Ehr+06]. Definition 2.2.3 (Gluing condition (DPO)) . Let p= (L , K , R , l , r) be a graph transformation rule, Ga graph, and m:L→Ga match. Then, •GP denotes those nodes and edges in L , called gluing points, that are not deleted by p, i.e., GP =l(K), •IP denotes those nodes and edges in L , called identification points, whose images under m have been merged into the same element in G , i.e., IP ={v∈ VL|∃w∈VL , w6=v:m(v) = m(w)} ∪ {e∈EL|∃ f∈EL , f6=e:m(e) = m(f)} , and •DP denotes those nodes in L , called dangling points, whose images under m are the source or target of an edge in G that is not contained in m(L) , i.e., DP ={v∈VL|∃e∈EG\m(EL):src(e) = m(v)∨tgt(e) = m(v)}. If all identification points and all dangling points are also gluing points, i.e., IP ∪DP ⊆ GP, then pand msatisfy the gluing condition (and thus pis applicable at m). If a DPO graph transformation rule is applicable at a match m , its graph transformation is defined by a double pushout in Graph. Definition 2.2.4 (Graph transformation (DPO)) . Let p= (L , K , R , l , r) be a graph transformation rule and m:L→G a match of its LHS L to a graph G such that p is applicable at m . The (direct) graph transformation 3 from G to H via p at m , written Gp,m =⇒H, is given by the pushouts (G,l∗,m)and (H,r∗,m∗)in Graph. 3A (direct) graph transformation is also known as (direct) derivation, cf. [Cor+97] 2.3. SINGLE PUSHOUT APPROACH 19 K R D H r r∗ km∗ L G l l∗ m(PO) (PO) The first pushout results in the construction of a context graph D , which corresponds to a temporary, intermediate graph where all deletion but no creation is performed. Then, the second pushout, which always exists if the first pushout exists, adds new elements of the rule’s RHS by gluing them together with the context graph. 2.3 Single Pushout Approach In the single pushout approach, graph transformation rules are defined by only one morphism. This morphism directly maps from the LHS to the RHS, without the use of a gluing graph. To allow the deletion of elements, this morphism is partial instead of total. Intuitively, elements of the LHS that are outside of the morphism’s restricted domain are deleted, and elements of the RHS that are outside of the morphism’s range are created. Definition 2.3.1 (Graph transformation rule (SPO)) . Agraph transformation rule p= (L , R , r) consists of two graphs L and R , called left-hand side (LHS) and right-hand side (RHS), and an injective partial graph morphism r:L→R , called rule morphism. In an SPO graph transformation rule, the rule morphism specifies both addition and deletion. Therefore, the pushout construction for the SPO approach is more complicated than for the DPO approach. In addition to the concept of gluing, it has to realize deletion. Deletion is realized in the SPO approach by “equalizing” two partial morphisms that are defined on the same domain of definition but on different restricted domains. This is done by removing all elements from their range that have different preimages under both morphisms. This concept is formalized by the categorical notion of a co-equalizer. The SPO approach constructs a specific co-equalizer, cf. [Ehr+97]. Its construction assumes that, for each element that is contained in the restricted domains of both morphisms, both morphisms map to the same image. We will see that this is sufficient for the construction of a pushout in GraphP , the category of graphs and partial graph morphisms, in Definition 2.3.3. Definition 2.3.2 (Specific co-equalizer in GraphP ) . Let a , b:A→B be two (partial) morphisms such that ∀x∈dom(a)∩dom(b):a(x) = b(x) . The co-equalizer of a and bin GraphPis the tuple (C,c)where •C⊆Bis the largest subgraph of B\a(dom(b)) \b(dom(a)) and •c:B→C, with dom(c) = C, is the identity morphism on C. 20 CHAPTER 2. BACKGROUND ON GRAPH TRANSFORMATIONS To construct C , the co-equalizer filters out from B all elements for which there is a preimage under one of the morphisms a or b that is not defined under the other morphism. Therefore, only elements remain in Cthat have either the same preimage(s) under both morphisms or no preimages at all. Dangling edges are deleted because the definition constructs C as the greatest subgraph of B\a(dom(b)) \b(dom(a)) , which is a graph-like structure containing dangling edges. The construction of a pushout in GraphP is realized via two pushouts in Graph and a co-equalizer, cf. [Ehr+97]. The total morphisms for the two pushouts in Graph are defined in dependence on the partial morphism of the pushout in GraphP . The co-equalizer is used to realize deletion in the construction of a pushout in GraphP. Definition 2.3.3 (Pushout in GraphP ) . Let b:A→B and c:A→C be two partial graph morphisms. The pushout over b and c in GraphP always exists and can be constructed in three steps: 1. Construct the pushout (C0 , A→C0 , C→C0) of the total morphisms dom(c)→ Cand dom(c)→Ain Graph. (gluing 1) 2. Construct the pushout (D , B→D , C0→D) of the total morphisms dom(b)→ A→C0and dom(b)→Bin Graph. (gluing 2) 3. Construct the co-equalizer (E , D→E) of the partial morphisms A→B→D and A→C→C0→Din GraphP. (deletion) The pushout over b and c in GraphP is the tuple (E , C→C0→D→E , B→D→E) . dom(c)A CC0 dom(b)B D E (PO) (PO) Since the pushout in GraphP always exists, there is no counterpart to the gluing condition in SPO. We can simply define the application of an SPO graph transformation rule as a pushout in GraphP. Definition 2.3.4 (Graph transformation (SPO)) . Let p= (L , R , r) be a graph transformation rule and m:L→G a match of its LHS L to a graph G . The graph transformation from G to H via p at m , written as Gp,m =⇒H , is given by the pushout (H,r∗,m∗)over rand min GraphP. L R GH r m r∗ m∗ (PO) The morphisms r∗ and m∗ are called the derivation morphism and the co-match of Gp,m =⇒H, respectively. 2.4. NACS, TYPES, AND VISUAL REPRESENTATION 21 The match m and the rule morphism r correspond to A→C and A→B of Definition 2.3.3, respectively. Since the match of an LHS to a host graph is always total, the first pushout in Graph does not do anything. The second pushout in Graph adds elements, similar to the second pushout during the application of a DPO rule. Due to the second pushout, A→B→D and A→C→C0→D commute, which allows to construct their co-equalizer. At the end, the co-equalizer deletes all elements for which there is a preimage under m that is not defined under r . Regardless of whether or not such an element has another preimage under m that is defined under r , the element is deleted. The existence of another preimage is not relevant, see Definition 2.3.2. To end up in a valid graph, the co-equalizer deletes dangling edges as well. 2.4 Negative Application Conditions, Types, and Visual Representation The visual representation of graph transformation rules used in this thesis follows the story pattern formalism [Det+12]. A story pattern represents a graph transformation rule by integrating the LHS and RHS into one graph and using stereotypes to indicate elements that are only present in the LHS or RHS. :RailCab :Track:Track:Track :RailCab:RailCab :Convoy:Convoy «++» on «++» member member on next on member next «- -» on Figure 2.1: An example of a story pattern Figure 2.1 shows a story pattern from one of the two RailCab domains used in this thesis. The story pattern shows a RailCab joining a convoy of RailCabs. Nodes and edges that are being created by the application of the story pattern, i.e., appear only in the RHS, or deleted, i.e., appear only in the LHS, are labeled with stereotypes «++» and «--» and drawn in green and red, respectively. Elements being created are also referred to as creation node/edge and elements being deleted as deletion node/edge. This story pattern specifies the creation of a member edge representing the RailCab’s participation in the convoy operation simultaneously with its movement to the next track segment. To restrict the applicability of a rule, a negative application condition (NAC) can be used. A negative application condition forbids specific graph structures from being present in the host graph. The story pattern formalism also allows to express negative application conditions. In Figure 2.1, the crossed out Convoy node and 28 CHAPTER 3. BACKGROUND ON AI PLANNING (RDDL) [San10]. It is the planning language currently used in probabilistic tracks of IPCs. For distributed and multi-agent planning, multiple planning languages have been proposed, some of them extensions to PDDL. The most recent and promising one is Multi-Agent PDDL (MA-PDDL) [Kov12]. It supports both planning for and planning by multiple agents, was used in 2015 during a multi-agent planning competition organized by the ICAPS Workshop on Distributed and Multi-Agent Planning (DMAP 2015), and is expected to become the input language for possible multi-agent planning tracks on future IPCs. For arbitrary planning problems in the propositional STRIPS formalism, deciding the existence of a plan is PSPACE-complete, cf. [Byl94]. If actions are only allowed to add but not to delete atomic formulas, it is NP-complete. Fortunately, in many transportation domains (where the consumption of fuel is not constrained), a satisfying plan can be found in polynomial time, cf. [Hel14]. However, finding a satisfying plan if fuel is restricted and finding an optimal plan both are NP-complete. 3.1 PDDL Fundamentals In PDDL, a planning task is separated into a domain and a problem description. A domain description characterizes the mechanics of a domain, i.e., it defines (parameterized) operations, called action schemata, as well as object types and predicates, which are used within those action schemata. Here, a predicate means the settheoretic meaning of a predicate, i.e., a Boolean-valued function. As usual, the term predicate refers to a predicate symbol (or name), and the term literal refers to an atomic formula, which is a predicate symbol together with a list of arguments, or its negation. Problem instance information, like specific objects available in the planning task’s “world”, are defined in problem descriptions. Such a problem description also defines an initial state, which is represented as a set of ground atomic formulas, and a goal specification. Multiple problem descriptions can be associated with the same domain description, thus yielding different planning tasks on the same application domain. Note that states follow the closed-world assumption: any atomic formula that is not known to be true in a state is indeed false. An action schema within a domain description consists of a list of parameters, a precondition, and an effect. In the precondition, a list of literals that are required for applying the action can be specified. Similarly, the effect of an action specifies a list of literals that are obtained when the action is applied. An action schema is instantiated – in the context of PDDL, this is called grounding – by substituting the list of parameters with objects defined in the problem description. Since the arguments of all literals are contained in the list of parameters, this transforms the literals into ground literals, which do not contain any free variables. Examples for a domain and an associated problem description are given in Listings 3.1 and 3.2. According to the domain description, vehicles can move between locations by consuming fuel. To capture this possibility, the domain declares the 3.1. PDDL FUNDAMENTALS 29 Listing 3.1: An example domain desciption in PDDL [FL03] 1: (define (domain vehicle) 2: (:requirements :strips :typing) 3: (:types vehicle location fuel-level) 4: (:predicates 5: (at ?v - vehicle ?p - location) 6: (fuel ?v - vehicle ?f - fuel-level) 7: (accessible ?v - vehicle ?p1 ?p2 - location) 8: (next ?f1 ?f2 - fuel-level) 9: ) 10: (:action drive 11: :parameters (?v - vehicle ?from ?to - location ?fbefore ?fafter - ⤦ ↪fuel-level) 12: :precondition (and 13: (at ?v ?from) 14: (accessible ?v ?from ?to) 15: (fuel ?v ?fbefore) 16: (next ?fbefore ?fafter) 17: ) 18: :effect (and 19: (not (at ?v ?from)) 20: (at ?v ?to) 21: (not (fuel ?v ?fbefore)) 22: (fuel ?v ?fafter) 23: ) 24: ) 25: ) types vehicle , location , and fuel-level and four predicates that state at which location each vehicle is (line 5), which fuel level each vehicle has (line 6), which location is accessible from which other location for each vehicle (line 7), and which fuel level follows which fuel level after fuel has been consumed (line 8). The action schema’s precondition ensures that the vehicle is at the starting position assumed by the ground action (line 13), the end position is accessible by the vehicle from the starting position (line 14), the vehicle has the fuel level assumed by the ground action (line 15), and a next lower fuel level exists (line 16). Its effect changes the vehicles position to the end location (lines 19 and 20) and reduces the fuel level of the vehicle (lines 21 and 22). Note that variable names always start with a question mark, and parameters of predicates or actions are denoted by variable names followed by their type. The given problem description defines two vehicles, three fuel levels, and four locations as available objects (lines 4 to 6). Its initial state defines dynamic state information, like the positions of vehicles and their fuel level (lines 9 to 12), but 30 CHAPTER 3. BACKGROUND ON AI PLANNING Listing 3.2: A problem description to the domain of Listing 3.1 [FL03] 1: (define (problem vehicle-example) 2: (:domain vehicle) 3: (:objects 4: truck car - vehicle 5: full half empty - fuel-level 6: Paris Berlin Rome Madrid - location 7: ) 8: (:init 9: (at truck Rome) 10: (at car Paris) 11: (fuel truck half) 12: (fuel car full) 13: (next full half) 14: (next half empty) 15: (accessible car Paris Berlin) 16: (accessible car Berlin Rome) 17: (accessible car Rome Madrid) 18: (accessible truck Rome Paris) 19: (accessible truck Rome Berlin) 20: (accessible truck Berlin Paris) 21: ) 22: (:goal (and 23: (at truck Paris) 24: (at car Rome) 25: )) 26: ) also static problem instance information, like the connections between different fuel levels and locations (lines 13 to 20). PDDL provides several extensions to the core functionality explained above, which essentially constitute the STRIPS formalism. The only extension already used in the examples shown above is typing, which allows to use a type hierarchy for objects. This extension is supported by every relevant PDDL-based planning system today. Unfortunately, other extensions are not supported universally; their support depends on the employed planning system. For example, the extension negative preconditions enables the use of negative literals in an action’s precondition, which is a very useful feature in domain modeling. Another extension, which is made use of in Chapter 6, is equality. It allows to use the equal sign as a predicate that is interpreted as equality. Disjunctions and quantifiers can be used in preconditions and goals via the extensions disjunctive preconditions and quantified preconditions, respectively. Universally quantified and conditional effects can both be supported via the extension conditional effects. 3.2. NUMERIC EXPRESSIONS 31 3.2 Numeric Expressions To support planning domains involving non-binary resources, version 2.1 of PDDL introduced numeric expressions. Numeric expressions use numeric-valued functions to associate values with objects of the domain. The declaration of these functions works analogously to that of predicates: it requires only a function name and a list of argument types. The support for numeric expressions can be enabled via the extension fluents. The value of a numeric-valued function for a specific list of arguments constitutes a primitive numeric expression. Values are not restricted or distinguished in what they represent; they can represent quantities of resources, counters, indices, or some dimension of utility. Using arithmetic operators, a numeric expression can be constructed from several primitive numeric expressions. Numeric expressions are only allowed to appear as part of numeric facts or numeric assignments. A numeric fact can be used to compare the values of two numeric expressions in an action’s condition or the condition of a conditional effect. A numeric assignment can be used in the effect of an action to assign a new value to a primitive numeric expression. Numeric expressions are not allowed in action parameters or as arguments to literals or other numeric expressions. Listing 3.3: A domain description with numeric expressions [FL03] 1: (define (domain jug-pouring) 2: (:requirements :typing :fluents) 3: (:types jug) 4: (:functions 5: (amount ?j - jug) 6: (capacity ?j - jug) 7: ) 8: (:action pour 9: :parameters (?jug1 ?jug2 - jug) 10: :precondition (>= (- (capacity ?jug2) (amount ?jug2)) (amount ?jug1)) 11: :effect (and 12: (assign (amount ?jug1) 0) 13: (increase (amount ?jug2) (amount ?jug1)) 14: ) 15: ) 16: ) An example using numeric expressions is given in Listing 3.3. The domain models an action of the jugs-and-water problem, where jugs of different sizes are available, and the goal is to achieve a certain filling level for each jug. There are two numeric-valued function in this domain: a function that yields the filling level of each jug (line 5) as well as a function that yields their holding capacity (line 6). The modeled action allows to pour the water contained in one jug into a second jug under the condition that the second jug has enough empty space left to hold the 32 CHAPTER 3. BACKGROUND ON AI PLANNING additional water. The precondition specifies this condition by use of a numeric fact calculating the empty space of the second jug and comparing it with the amount of water in the first (line 10). The effect specifies two numeric assignments: the first is an absolute assignment that empties the first jug (line 12); the second is a relative assignment increasing the amount of water in the second jug by that of the first jug (line 13). Along with numeric expressions came plan metrics, which evaluate the quality of plans based on numeric expressions. A plan metric can be provided in the problem description to define an objective for the planning process different from minimizing the number of used actions (in sequential planning) or the timespan of the entire plan (in temporal planning). An example of a plan metric for the vehicles domain is to minimize the amount of fuel used by each vehicle. Obviously, the domain has to specify a suitable function for representing this quantity and update its values each time fuel is consumed. Note that this thesis does not make use of plan metrics other than the built-in metric total-time, which refers to the plan’s timespan. 3.3 Durative Actions Like numeric expressions, durative actions have been introduced in version 2.1 of PDDL. There are two kinds of durative actions: discretized and continuous durative actions. Here, we consider discretized durative actions only. Durative actions split the literals, numeric facts, and numeric assignments used in each their precondition and effect into different sets according to their time of evaluation. They can be required at_start , over_all , and at_end when used in the precondition and be effective at_start and at_end when used in the effect. While at_start and at_end refer to the beginning and ending of an action, over_all refers to the (open) interval during the action’s execution. As a result, a durative action behaves like two untimed but temporally linked actions with an invariant condition that must be met by all states occurring during their application interval. Without a notion of time, plans were simply interpreted as sequences of states. With durative actions, the application intervals of actions can overlap, which leads to the question under what constraints they are allowed to do so. To answer this question, we first take a look at the notion of states in this temporal context. States are stretched over intervals, which are separated by points in time on a global clock. State change occurs only at those points in time, and all state change at a given time point occurs instantaneously. The time points where state changes occur are given by the beginnings and endings of durative actions. Multiple beginnings or endings of different actions may fall at the same point in time if their conditions and effects do not interfere. In the semantics of durative actions, such a set of action beginnings and endings is called a happening and treated like an ordinary untimed action. Within a happening, it is not allowed to assert a literal and its negation at the same time. It is also forbidden to assert a literal at the same time it is required by another action’s beginning or ending in the same happening. No condition may rely on an effect in the same happening. Even if the condition is true before and 3.4. REQUIRED CONCURRENCY 33 after executing a concurrent effect, it may not rely on the value of a literal if the effect updates the value. Fox and Long [FL03] called this the no moving targets rule. Note that the beginning or ending of a single action is allowed to access a value in its condition and update it in its effect at the same time. This is only forbidden if performed by different actions, essentially like mutual exclusion for shared variables. A similar restriction holds for numeric facts and assignments in happenings. The only difference is that multiple simultaneous updates are allowed if they commute, i.e., each of them is a relative assignment. A consequence of the no moving targets rule is a non-zero separation between each pair of happenings: unlike timed automata and related constructs, where the passing of time is not required between two successive changes of the logical state, two happenings have to occur at least a minimum time of ε> 0 apart from each other. Temporal planning systems often use a value of 0.001 as minimum unit of time. Durative actions complicate the picture of a planning task’s state space in that they involve a commitment. A durative action that has been started in a state, has to be finished at a later point in time. All states up to this point in time have to fulfill the over_all conditions of the durative action, and the state at this point in time has to fulfill its at_end conditions. However, since the at_end condition does not have to be fulfilled when the action starts, it can be achieved by concurrent actions. For this reason, the decision whether a durative action is applicable cannot be made alone by looking at all actions that have been applied already. Instead of defining the semantics of durative rules in terms of state space construction, Fox and Long [FL03] defined it in terms of executability of happening sequences. Each happening has to fulfill the no moving targets rule, their accumulated action beginnings and endings have to be executable in the order given by the happening sequence, and the state resulting by executing the complete happening sequence has to satisfy the goal specification of the planning task. The happening sequence also contains artificial monitoring actions responsible for checking invariant conditions. These monitoring actions do not contain any effects. They are placed after a durative action with invariant conditions has been started and after each other happening occurring during its application interval. Note that the search through the state space might also consider happening sequences that are not executable, because additional durative actions enabling their executability have not yet been scheduled. 3.4 Required Concurrency The introduction of durative actions into planning domains added a scheduling problem to the planning tasks. A widely used approach to solve these planning tasks is to separate logical from temporal reasoning and solve the planning and scheduling problems separately. By treating durative actions as single instantaneous actions – this is called action compression [LF03] – and thus neglecting any opportunities for the concurrent execution of actions, a plan is computed by employing a classical 34 CHAPTER 3. BACKGROUND ON AI PLANNING sequential planner. Afterwards, actions are scheduled in a post-process to achieve a better plan length. As one might expect, such a pragmatic approach is very fast. Unfortunately, approaches that separate planning and scheduling are not complete. There are planning problems for which no sequential solution exists. A planning problems where at least one action has to be applied concurrently to another action in order to reach the goal is said to have required concurrency. Such a planning problem cannot be solved by a sequential planning system. If a planning problem with required concurrency can be formulated on a planning domain, this domain is said to support required concurrency. Note that a planning problem on a domain supporting required concurrency does not automatically have required concurrency itself; it is easily possible to model a planning problem without required concurrency on any domain. While the term required concurrency was coined by Cushing et al. [Cus+07] in 2007, it has been known before that planning systems solving temporal planning tasks via action compression and sequential planning, like SGPlan [CWH06] or MIPS [Ede03], are fast but not complete. Temporal planning systems that did not perform action compression, like LPGP [LF03] or VHPOP [YS03], were not competitive. For this reason, Halsey et al. [HLF04] developed a planning system that integrates scheduling phases into the planning phase. Its idea is to integrate scheduling phases only where necessary, but postpone scheduling where possible, without sacrificing completeness. Their planner CRIKEY and its successors CRIKEY SHE [Col+09b] and CRIKEY3 [Col+08] detect situations where this integration is necessary by identifying specific patterns in conditions and effects of actions. If such a pattern is found in an action, its ending is considered a choice point for state space exploration; otherwise it is simply applied directly or as soon as it is needed [Col+09a]. CRIKEY3 provides the code base for several state-of-the-art planning systems developed by the Planning Group at King’s College London 1 , among them the temporal planning system POPF [Col+10], which is used in Chapter 6 for evaluating different planning domains with required concurrency. 1 The Planning Group of Maria Fox and Derek Long moved from the University of Strathclyde to King’s College London in 2011. 4 Planning with Graph Transformations This chapter presents an approach that allows technical systems to autonomously decide how to reconfigure their software architecture by performing planning tasks on graph transformation systems. Focusing solely on structural aspects, this approach excludes any timing and concurrency issues. This allows to use ordinary (typed) graph transformation rules to model possible reconfigurations of the system. Classical planning approaches for fully observable and deterministic environments work with notions of state and action: the execution of an action results in a state change. In the case of graph transformation planning, states are represented as graphs, and those actions available in a planning domain result from a set of graph transformation rules. More precisely, a graph transformation rule is a parameterized action and graph transformations are grounded actions in which elements of the LHS have been substituted with elements from the host graph. The transition system of a graph transformation system can be constructed by successively applying graph transformations to the initial graph and its successor graphs. The planning task is to find a path in this transition system ending in a graph satisfying a goal specification. The transitions on this path constitute the plan. Since the transition system suffers from a state explosion problem, i.e., a combinatorial blowup of the state space, constructing the complete transition system is not an appropriate option to find a plan. To find a plan efficiently, we need a suitable planning technique. Planning with graph transformations has been covered before, e.g., in [EW11] for coordinating behavior in cyber-physical systems and in [TK11] for planning a self-healing process in automotive systems. The planning problems are usually solved by one of the following two approaches: either a translation into a dedicated planning language, like PDDL, is performed or a planning system is developed that works directly on a graph transformation system. Unfortunately, both approaches have their drawbacks. Employing a translation-based approach is tempting because it exploits decades 35 36 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS of research in AI planning by applying state-of-the-art planning systems. However, translation-based approaches suffer from a different expressiveness of GTSs and PDDL: while the creation and deletion of nodes is a fundamental feature of graph transformation systems, there is no such thing in PDDL. By not supporting the instantiation and deinstantiation of objects, PDDL maintains a finite state space. In order to handle the object instantiation and deinstantiation in PDDL nevertheless, a modeling workaround can be used that declares all uninstantiated objects in the initial state, but uses a predicate to state their actual existence. However, the workaround is based on the assumption that a maximal number of objects is known beforehand or can be deduced from the graph transformation system. Unfortunately, planning systems working directly on the transition system of a graph transformation system are not highly evolved. Up until today, there are only few systems that use domain-independent heuristics to guide their search through the state space of a graph transformation system. Their domain-independent heuristics are rather simple: they compute values for the structural similarity of the current configuration and the goal specification. Multiple such similarity-based heuristics are presented in [EJL06]. Several of them are different variants of counting those nodes and edges that have to be created or deleted to reach a target configuration, e.g., they differ in whether or not it is allowed to rely on the identity of nodes and edges, and then using this number as a distance measure. A slightly different variant of such a heuristic has also been presented in [Sni11]. Another idea for a similarity-based heuristics given in [EJL06] is to transform the goal specification into a formula and evaluate how many predicates of this formula are false in a given state. Other graph transformation planning systems not employing domain-independent heuristics, e.g., semi-automatically deducing domain-specific heuristics based on expert knowledge [EW11] or performing entirely different kinds of analyses to guide the search in the state space [HHV11], are explained in more detail in Section 4.5, the related work section of this chapter. A problem of the aforementioned similarity-based heuristics is that they do not take any graph transformation rules into account. A high similarity between the current state and the goal specification is irrelevant if there are no rules available that can efficiently transform the current state into a state satisfying the goal specification. Therefore, we believe that it is mandatory for an efficient planning system working directly with graph transformations to look into search techniques of state-of-the- art AI planning systems. Adapting already established techniques from modern PDDL-based planners to graph transformation systems might be straightforward in some cases or impossible due to the different expressiveness of graph transformation systems and PDDL in other cases, e.g., due to the possibility of instantiating nodes in graph transformation systems. Furthermore, the process of adapting such techniques might lead to ideas that were impossible or very unintuitive in PDDL-based representations, e.g., merging of nodes. This renders the adaptation of known planning approaches to graph transformation systems an interesting research perspective. We developed a new planning system working with graph transformations, cf. [Zie14]. It employs a domain-independent heuristic function, which can be used 4.1. PROBLEM STATEMENT 37 in combination with different search algorithms. The heuristic function is mainly inspired by the planning system Fast-Forward (FF) [HN01], which is a forwardchaining planner with a heuristic function that uses the solution length of a relaxed problem as heuristic estimate. It won the 2nd International Planning Competition (IPC-2000), which led to a shift of planning research towards heuristic-guided approaches. Variants of its techniques are used in many of today’s state-of-the-art planners, e.g., LAMA [RW10a]. In our approach, the relaxation is performed by reinterpreting certain parts of the rules’ application conditions. Thanks to this reinterpretation, the relaxed problem is easier to solve than the original problem. As part of this contribution, we compare the performance of our heuristic against the performance of a similarity-based heuristic. The next section introduces the notion of planning problems on graph transformations systems. The reconfiguration of ECUs serves as a running example for this chapter. Its graph transformation system is presented in Section 4.2 and used in Section 4.3 to explain our heuristic approach. An evaluation comparing the performance of our heuristic against the performance of a similarity-based heuristic is given in Section 4.4. We discuss related work in the narrow area of graph transformation planning in Section 4.5. Then, we conclude this chapter with a discussion on the differences of our heuristic function to that employed by FF and an outlook on further possibilities for graph transformation planners in Section 4.6. 4.1 Problem Statement To define the graph transformation planning problem, we first need a means to specify a goal. Such a goal specification can, for example, be a graph, which has to be found by the planning system by applying graph transformations to the initial graph. In general, we do not search for the exact graph but for a larger graph that contains the graph we are looking for as a subgraph. We also do not require the same identity of nodes and edges, i.e., we search for a subgraph isomorphism. Goal specifications also supports NACs. Therefore, a goal specification is sort of like a graph transformation rule without an RHS. We call this a graph pattern. Definition 4.1.1 (Graph pattern) . Agraph pattern P= (L , N) consists of a graph L and a set of NACs N where each NAC ∈ N is a tuple NAC = (N , n) with n:L→Nand nbeing injective. NAC satisfaction is defined as in Definition 2.4.1. Having a means of specifying target configurations of a planning problem, we can now define the planning problem itself. Definition 4.1.2 (Graph transformation planning problem) . Agraph transformation planning problem P= (G0,R,Ptgt)consists of • an initial graph G0, • a set of graph transformation rules R, and • a target graph pattern Ptgt = (Ltgt,Ntgt). 44 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS Table 4.1: Rule application labels of the first abstract successor state Element Attached labels i1 ‹#1, ’destroyInst.’, #1› i2 ‹#1, ’destroyInst.’, #2› inst(c1,i1) ‹#1, ’destroyInst.’, #1› inst(c2,i2) ‹#1, ’destroyInst.’, #2› running(i1,n1) ‹#1, ’destroyInst.’, #1› running(i2,n2) ‹#1, ’destroyInst.’, #2› deployed(c1,n2) ‹#1, ’deployComp.’, #1› deployed(c2,n1) ‹#1, ’deployComp.’, #2› generated x successor states, where x is two times the heuristic value of the initial state of the concrete planning problem. This ensures that the computation of a heuristic value terminates and that the search algorithm can continue with other states if the relaxed problem is not solvable from a certain state. 4.3.2 Rule Application Labels Our planning system performs a state space exploration by successively choosing a state and expanding it, i.e., applying each rule at each possible match to generate its successor states. To decide which state to expand next, the system calculates a heuristic value for each unexpanded state. Calculating a heuristic value for a state involves generating the abstract state sequence starting in this state until we reach a state that satisfies the target graph pattern. Having constructed the abstract state sequence, a naive idea would be to use its length as heuristic estimate. Although the abstract state sequence is expected to be shorter for states which are near to a goal state and longer for states which are further away from a goal state, this value is still rather imprecise. A better idea is to give the approximate number of individual graph transformations needed for reaching the (abstract) goal state. However, we cannot simply count all applied transformations per transition to calculate this number, because this would include a lot of transformations that were not needed to reach the (abstract) goal state. The transformations that were needed to reach the (abstract) goal state are called a relaxed plan and their number is called the length of the relaxed plan. Our approach to calculate this number incorporates rule application information into the newly created elements of each successor graph. Each created element is labeled with information about the transformation that caused its creation. This label consists of the iteration number of the successor graph creation loop, the name of the applied rule, and a distinct identifier for the match of the rule to the host graph. As an example, the deployed edge from component c1 to ECU n2 is labeled with ‹iteration #1, ’ deployComponent ’, match #1›, see Table 4.1 and the second state in Figure 4.5. When the goal match is found, we can count the number of distinct rule appli- 4.3. RELAXED PLANNING HEURISTIC 45 Table 4.2: Rule application labels of the second abstract successor state Element Directly attached labels Propagated labels i1 ‹#1, ’destroyInst.’, #1› i2 ‹#1, ’destroyInst.’, #2› inst(c1,i1) ‹#1, ’destroyInst.’, #1› inst(c2,i2) ‹#1, ’destroyInst.’, #2› running(i1,n1) ‹#1, ’destroyInst.’, #1› running(i2,n2) ‹#1, ’destroyInst.’, #2› deployed(c1,n2) ‹#1, ’deployComp.’, #1› deployed(c2,n1) ‹#1, ’deployComp.’, #2› i3 ‹#2, ’createInst.’, #1› ‹#1, ’destroyInst.’, #1› i4 ‹#2, ’createInst.’, #2› ‹#1, ’destroyInst.’, #2› i5 ‹#2, ’createInst.’, #3› ‹#1, ’deployComp.’, #1› i6 ‹#2, ’createInst.’, #4› ‹#1, ’deployComp.’, #2› inst(c1,i3) ‹#2, ’createInst.’, #1› ‹#1, ’destroyInst.’, #1› inst(c2,i4) ‹#2, ’createInst.’, #2› ‹#1, ’destroyInst.’, #2› inst(c1,i5) ‹#2, ’createInst.’, #3› ‹#1, ’deployComp.’, #1› inst(c2,i6) ‹#2, ’createInst.’, #4› ‹#1, ’deployComp.’, #2› running(i3,n1) ‹#2, ’createInst.’, #1› ‹#1, ’destroyInst.’, #1› running(i4,n2) ‹#2, ’createInst.’, #2› ‹#1, ’destroyInst.’, #2› running(i5,n2) ‹#2, ’createInst.’, #3› ‹#1, ’deployComp.’, #1› running(i6,n1) ‹#2, ’createInst.’, #4› ‹#1, ’deployComp.’, #2› down(n1,n1) ‹#2, ’shutdownEcu’, #1› ‹#1, ’destroyInst.’, #1› down(n2,n2) ‹#2, ’shutdownEcu’, #2› ‹#1, ’destroyInst.’, #2› cation labels that are contained in the elements of the goal match. This number is the number of transformations needed to create the elements in the goal match. However, these labels contains only labels of elements that appear directly in the goal match. It does not yet contain labels of elements that were needed to arrive at the goal match. An example for this is the label of the aforementioned deployed edge from component c1 to ECU n2 . While the deployed edge is not contained in the goal match, its creation during the first transition was necessary for the application of another transformation during the second transition to create an element in the goal match. In this example, the application of createInstance that creates component instance i5 during the second transition required the deployed edge from c1 to n2 . Our approach includes labels of such elements when counting the rule application labels in the goal match: each element created by a transformation – in addition to its own label – inherits the labels of all elements in the LHS match of the rule application. In the example above, the rule application label of the deployed edge created during the first transition is propagated to the newly created instance i5 during the second transition, see Table 4.2 and the third state in Figure 4.5. Elements that have been marked as deleted are handled similarly. For example, the component instance i1 receives the rule application label ‹iteration #1, 46 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS ’ destroyInstance ’, match #1› when it is marked as deleted by the application of the destroyInstance rule, see Table 4.1. Labels of elements being marked as deleted are propagated to newly created (or deleted) elements if the labeled element is contained in a NAC match, e.g., the label of i1 is propagated to the down edge at ECU n1 when shutdownNode is applied during the second transition, see Table 4.2. Note that elements being marked as deleted inherit labels in the same manner as elements marked as created: they inherit labels of created elements if contained in the LHS match and labels of deleted elements if contained in the NAC match. By inheriting the labels of other elements, the elements in the goal match do not only contain labels of transformations that directly created them, but also about all prior transformations that made their creation possible – whether by means of element creation or deletion. The heuristic value is now simply defined as the number of rule application labels that are attached to all elements in the goal match. This is reasonable because rule application labels have been propagated to elements in the goal match if the referenced rule application assisted in establishing the goal match. In doing so, counting rule application labels follows set semantics, i.e., if elements that were created from different transformations share the same inherited labels, these labels are counted only once. In general, the rule application label set contains at least one label for each iteration of the successor graph creation loop. Applied to the example of Figure 4.5, the goal match containing i5 and i2 results in a heuristic value of 4. This value comes from two rule application labels of i5 and the two of n1 ’s down edge. The rule application label of i2 is not counted, because i2 is marked as deleted. It would have been counted if i2 was contained in a NAC. When there exist multiple goal matches present in an abstract state, we use the smaller value. This prevents from basing the heuristic value on a goal match containing i4 instead of i2 . If we had not used the NAC for the running edge between the component instance of c1 and n1 in the target graph pattern, a goal match containing i1 and thus a heuristic value of 2 would also have been possible. However, since we knew from the initial configuration that i1 is running on an ECU that is supposed to be shut down, specifying this NAC was reasonable to prevent such an unfavorable goal match from being possible. 4.3.3 Program Code The heuristic function incorporates two important functionalities. The first functionality is the use of markings during the creation of abstract successor graphs. These markings allow to reinterpret NAC matching such that an element contained in the match of a NAC can be disregarded if it is marked as created or deleted. As a consequence, the use of these markings relaxes NAC matching and enables – together with the relaxed LHS matching, which results from not deleting elements when transformations are applied – the parallel execution of all applicable transformations. The second functionality is the use of rule application labels and their propagation to newly created or deleted elements. These labels allow to count those 4.3. RELAXED PLANNING HEURISTIC 47 rule applications that assisted in reaching the (abstract) goal state, which constitutes the heuristic value. Next, we provide program code for this heuristic function. It is divided into three procedures. The first procedure implements the relaxed NAC matching functionality. The second procedure is a simple helper function that collects rule application labels from elements in the LHS match. The third procedure realizes the heuristic function and calls the other two procedures to do so. Algorithm 4.1: Relaxed NAC matching Input: Match m:L→G, NACs N, Set labels Output: Boolean allNacsOk, Set labels 1: procedure checkAllNacMatches(m,N,labels) 2: for all q:N→Gwith (N,n)∈ N and q◦n=mdo 3: thisNacOk ←f alse 4: for all e∈ran(q)with e/∈ran(m)do 5: if eis marked as created then 6: thisNacOk ←true 7: break .no need to check other elements 8: end if 9: if eis marked as deleted then 10: thisNacOk ←true 11: insert labels attached to einto labels 12: break .no need to check other elements 13: end if 14: end for 15: if ¬thisNacOk then 16: return f alse .no need to check other NAC matches 17: end if 18: end for 19: return true 20: end procedure The first procedure, checkAllNacMatches, is given in Algorithm 4.1. Given an LHS match and the NACs of a graph transformation rule, it checks for each match of a NAC (line 2) whether it contains an element (line 4) that may be disregarded because it has been marked as created (line 5) or deleted (line 6). If such an element has been found, the current NAC match can be neglected under relaxed NAC matching. This also means that it is not necessary to check any remaining elements in this NAC match (lines 7 and 12). Note that elements that are already contained in the LHS are not considered by this check (line 4), because it is not reasonable to regard them as existing for LHS matching but as not present for NAC matching. As soon as a single NAC match is found that contains no element marked as either created or deleted, we know that this NAC is not satisfied, despite the applied relaxation. In such a case, there is no need to check any remaining NACs and 48 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS the procedure returns f alse (line 16). If each NAC match can be neglected due to marked elements, the procedure returns true (line 19). As a side effect, this procedure collects rule application labels from those elements that allowed neglecting a NAC match (line 11). This is only done for elements marked as deleted but not for elements marked as created, because you need to apply a transformation for deleting elements but not for not creating them. Note that the set of rule application labels is given as a reference, i.e., there is no need to return this set. Algorithm 4.2: Collecting rule application labels from an LHS match Input: Match m:L→G, Set labels Output: Set labels 1: procedure collectRuleApplicationLabels(m,labels) 2: for all e∈ran(m)do 3: if eis marked as created then 4: insert labels attached to einto labels 5: end if 6: end for 7: end procedure The second procedure, collectRuleApplicationLabels, is given in Algorithm 4.2. All it does is collect rule application of those elements that are marked as created. It is called from the third procedure, either with an LHS match or with a goal match as parameter. The procedure realizing the heuristic function, computeHeuristicValue, is given in Algorithm 4.3. Given the set of graph transformation rules, an initial graph for the relaxed problem, the target graph pattern, and an upper bound for the length of the abstract state sequence, it constructs successor states until either the most recently created successor state satisfies the target graph pattern or the upper bound is reached (line 4). The successor graph creation loop is roughly dividable into two parts. The first part (lines 5 to 20) constructs the next abstract successor state. The second part (lines 22 to 29) checks whether it satisfies the target graph pattern. To construct an abstract successor state, the procedure first searches all LHS matches of all graph transformation rules and checks whether all their NAC matches are satisfied under relaxed NAC matching by calling the procedure checkAllNac- Matches (line 9). For all LHS matches that satisfy their NAC matches, new elements are created according to the rule morphism, but none are deleted (line 11). Then, these new elements are marked as created (line 12), and elements supposed to be deleted according to the rule morphism are marked as ‹(line 13). Note that each of these elements is only marked if it has not been marked before. After the marking of elements is completed, the procedure attaches rule application labels to newly marked elements. Labels of elements that enabled the rule application by being marked as deleted, i.e., they allowed to neglect one of the 4.3. RELAXED PLANNING HEURISTIC 49 Algorithm 4.3: Heuristic function yielding the length of a relaxed plan Input: Rules R, Graph G0, GraphPattern Gtgt, Integer maxLength Output: Integer heuristicValue 1: procedure computeHeuristicValue(R,G0,Gtgt,maxLength) 2: G←G0 3: length ←0 4: while length ≤maxLength do 5: Gsucc ←G 6: for all p= (L,R,r,N)∈Rdo 7: for all m:L→Gdo 8: labels ←∅ 9: allNacsOk ←checkAllNacMatches(m,N,labels) 10: if allNacsOk then 11: add created elements of Gp,m =⇒Hto Gsucc 12: mark created elements of Gp,m =⇒Hin Gsucc as created 13: mark deleted elements of Gp,m =⇒Hin Gsucc as deleted 14: collectRuleApplicationLabels(m,labels) 15: insert ‹length,p.name, m.id› into labels 16: attach labels to newly marked elements in Gsucc 17: end if 18: end for 19: end for 20: G←Gsucc 21: length ←length +1 22: for all g:Ltgt →Gwith Gtgt = (Ltgt,Ntgt)do 23: labels ←∅ 24: allNacsOk ←checkAllNacMatches(g,Ntgt,labels) 25: if allNacsOk then 26: collectRuleApplicationLabels(g,labels) 27: return cardinality of labels 28: end if 29: end for 30: end while 31: return highest possible value of Integer 32: end procedure NAC matches, are already contained in the set labels due to a side effect of the procedure checkAllNacMatches (line 9). Now, the procedure also collects labels from elements that made the LHS match possible, i.e., elements that are marked as created and contained in the LHS match, by calling the procedure collectRuleApplicationLabels (line 14). Then, it also puts a label for the rule application that was just executed into the set labels (line 15) and attaches this set to all elements that have been marked as created or deleted by this rule application (line 16). As 50 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS a consequence, each element is labeled with both a label for the rule application that created the element and/or its marking as well as labels that made this rule application possible. After the next abstract successor state has been created, the procedure checks whether this state satisfies the target graph pattern. Like the application of graph transformation rules, this check is performed under relaxed NAC matching (line 24). In case it does satisfy the target graph patten, the procedure collects labels from elements that are marked as created and contained in the goal match before returning the size of this set as heuristic value. Labels from elements marked as deleted have already been collected when checking relaxed NAC matching. 4.4 Evaluation We compared the performance of our relaxed planning heuristic ( hrp ) against that of a similarity-based heuristic ( hsim ), which resembles those heuristic functions employed by Edelkamp et al. [EJL06] and Snippe [Sni11]. The similarity-based heuristic counts the number of nodes and edges that exist in both the current configuration and the target configuration. It relies on the types of nodes and edges to judge whether a node or edge is counted as existing. More precisely, it puts the type of each node and edge of a configuration into a multiset and takes the cardinality of the intersection of the current configuration’s multiset and the target configuration’s multiset as a similarity measure. The heuristic value is then defined as the additive inverse of this measure. Both heuristics have been implemented in GROOVE [Ren04]. To eliminate any potential side effects with a particular search algorithm, each of the heuristics was employed multiple times in combination with a different search algorithm. This evaluation was performed on two different problem domains. Search algorithms Both heuristic functions were evaluated in combination with greedy best-first and a variant of enforced hill-climbing. Greedy best-first (GBF) [RN03] is a well-known search algorithm for informed search. It uses a closed list and an open list of states. After expanding a state, i.e., all successor states have been generated, this state is placed in the closed list. For each new successor state found, its heuristic value is computed and then the state is placed in the open list. The decision which state to expand next is solely based on the heuristic values of the states in the open list. The costs to reach the current state are not considered. As a result, the algorithm greedily chooses among all known states that state with the smallest expected distance to the goal state. We also tested a variant of GBF that differs from this approach in that it also greedily expands the next state, cf. [CS07, Sect. 3.2]. If a successor state with a better heuristic than the current state is found, this variant immediately chooses this state to expand, without checking any remaining sibling states. When this happens, the current state is not placed in the closed list; it remains in the open list, directly behind the new state. By doing so, the heuristic values of its remaining successor 4.4. EVALUATION 51 states can be computed later if the new state turns out to lead to worse successor states. Since there was no significant difference in performance between those two variants of GBF, this section includes only results of the traditional variant. Enforced hill-climbing (EHC) [HN01] is a local search algorithm. In each iteration it performs a breadth-first search from the current state until it finds a state with a better heuristic value. When such a state is found, it updates the current state and continues with the next iteration. We use a modified EHC that applies best-first search instead of breadth-first search in each iteration. This results in different behavior if EHC encounters plateaus, i.e., regions in the state space where the heuristic values of all successor states are not lower than the current best heuristic value. Using a best-first search rather than a breadth-first search is expected to result in shorter planning times or yield shorter plans on some domains, cf. [CS07, Sect. 6.3]. Problem domains The two problem domains used for our experiments are Blocks World and ECUs. Blocks World is a classical problem domain in the area of AI planning. It consists of a table with a set of cubes that can be stacked upon each other. A cube can only be moved if there are no other cubes on top of it, and there is only one arm that can hold a cube, i.e., two cubes cannot be moved simultaneously. Finding an optimal solution in this domain has been shown to be NP-hard [GN92]. The ECUs domain works as explained in Section 4.2. In contrast to the Blocks World domain, which does not involve the object instantiation, the ECUs domain contains rules creating new nodes. Experiment setup For the Blocks World domain, we used 8 different problem sizes (4, 6, 8, 10, 12, 14, 16, and 18 blocks) and 4 different problem instances (2 random initial and 2 random target configurations) per problem size. For the ECUs domain, we used 4 different problem sizes (2, 3, 4, and 5 ECUs), each with 4 different problem instances. Two of these problem instances had the same number of component instances running in the initial configuration as ECUs were available. The other two problem instances had an additional component instance running. Each target configuration specified every second ECU (rounding down at odd numbers of ECUs) to be shut down. The experiments were conducted on a Dual Intel Xeon E5520 compute server with 16 (virtual) cores running at 2.27GHz. Each experiment was given 4 cores and 4GB of RAM. If no plan could be computed within 20 minutes, the job was terminated. Results First, we give an overview of the number of explored states for each combination of heuristic function and search algorithm. The number of explored states counts only those states that have been chosen for expansion and is generally less than the number of all generated states. Therefore, it is a suitable measure for 52 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS 1 10 100 1000 10000 100000 1e+06 4blocks 6blocks 8blocks 10 blocks 12 blocks 14 blocks 16 blocks 18 blocks No. of explored states GBF/hsim EHC/hsim GBF/hrp EHC/hrp Figure 4.6: Histogram of the number of explored states in Blocks World domains 1 10 100 1000 10000 100000 1e+06 2ECUs 3ECUs 4ECUs 5ECUs No. of explored states GBF/hsim EHC/hsim GBF/hrp EHC/hrp Figure 4.7: Histogram of the number of explored states in ECUs domains 4.4. EVALUATION 53 how well the employed heuristic prunes the state space. Note that this number also does not include abstract states computed by hrp. Figure 4.6 shows a histogram of the average number of states for the BlocksWorld domain, Figure 4.7 for the ECUs domain. Note the logarithmic scale in both histograms. With increasing problem size hrp makes its superiority clear. Combinations with hsim failed to provide a solution within 20 minutes for the problems of size 10 blocks and above (on the BlocksWorld domain) and 5 ECUs (on the ECUs domain). There is no significant difference in performance between GBF and EHC. Considering the average planning times in Figures 4.8 and 4.9, we can observe that hsim performs better than hrp on small domains. The performance of hrp on small domains is worse than that of hsim because the computation costs of finding a relaxed plan is in general much higher than the computation costs of counting the number of nodes and edges in a state. However, the performance changes to the favor of hrp as the problem size increases: the planning time of hrp scales better than the planning time of hsim . This is expected because the number of generated states also scales better. Note the small discrepancy between the number of explored states and the total planning time in the case of 5 ECUs. The number of explored states did not increase when switching from instances with 4 ECUs to instances with 5 ECUs, whereas the planning time did increase. This can be explained via the number of generated states. The number of generated states increased when switching from instances with 4 ECUs to instances with 5 ECUs. This led to more heuristic values being calculated, which in turn led to more and better candidates being available for further exploration. Better candidates led to a smaller number of states chosen for exploration due to a smaller average plan length. Table 4.3: Percentage of time spent calculating heuristic values in BlocksWorld domains #blocks 4 6 8 10 12 14 16 18 GBF/hsim 4,58 3,44 4,97 — — — — — EHC/hsim 4,83 3,56 4,18 — — — — — GBF/hrp 89,80 93,65 94,31 95,16 97,28 97,81 99,40 99,02 EHC/hrp 88,10 92,67 94,62 95,24 97,32 97,77 99,14 99,37 Table 4.4: Percentage of time spent calculating heuristic values in ECUs domains #ECUs 2 3 4 5 GBF/hsim 3,70 5,02 3,95 — EHC/hsim 3,99 6,74 9,87 — GBF/hrp 87,32 94,15 98,38 99,58 EHC/hrp 81,60 91,88 98,46 99,74 Next, we take a detailed look at the time spent for calculating heuristic values. Tables 4.3 and 4.4 show these times in percentage of total planning time. While hsim consumes only approx. 4% of the total planning time, hrp consumes over 81%, 60 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS literal layer and an action layer together form a so-called step of the planning graph. Each later step also contains two such layers. The i -th literal layer contains those literals that can be asserted within i steps. The i -th action layer contains those actions that are applicable given the i -th literal layer. Note that the first two layers form step 0. A planning graph has edges between nodes of different layers that mirror the conditions and effects of actions. If a literal in step i is contained in the precondition of an action in step i , there is an edge from the literal to the action. If an action in step i asserts a literal in step i+ 1, there is an edge from the action to the literal. These edges enable to consider the relation between literals and actions when searching through the planning graph for a plan. In general, planning graphs also have mutual exclusion edges between actions that interfere with one another and between literals that cannot be achieved at the same step simultaneously. However, in the case of a relaxed planning task, there are no mutual exclusion edges because no literal is ever deleted, i.e., the relaxed planning graph is a bipartite graph. If a layer is reached that contains all goal literals, a backward search for a plan is performed. This is done by selecting an achiever, i.e., a (ground) action asserting the literal, for each literal in the goal set. Then, this selection is recursively applied for all literals in the preconditions of the selected actions. When this search reaches the first step, no actions need to be selected anymore and the set of selected actions constitutes the plan. Note that in general, the backward search for a plan can require backtracking when no action can be selected that is not exclusive to actions selected earlier. Since there are no mutual exclusion edges in a relaxed planning graph, no backtracking occurs here. This is what makes the search for a relaxed plan in a planning graph much more efficient than the search for a non-relaxed plan. By applying the idea of relaxed planning to graph transformation systems instead of PDDL’s propositional state representations, we face multiple differences. These differences stem from the fact that graph transformation systems, unlike PDDL, support object instantiation and from the integration of NACs into the abstract planning algorithm. Achievers and admissibility In FF’s relaxed planning graph, a literal can have multiple achievers. A relaxed plan is found by choosing an achiever for each literal in the goal match and for each unfulfilled literal in the precondition of other achievers. Finding the optimal relaxed plan, which results in an admissible heuristic, is NP-hard, cf. [Byl94]. Therefore, FF uses a heuristic for selecting achievers, which prefers those actions whose preconditions are easier to fulfill. While this does not result in an admissible heuristic anymore, it works well in practice and allows to find a relaxed plan in polynomial time. In our case, there are no multiple achievers for created elements. Each created element has a rule application label identifying the graph transformation that created it. Therefore, no search for an optimal set of achievers is necessary for created elements. Elements marked as deleted also have only one rule 4.6. DISCUSSION 61 application label, i.e., the label from the first rule application that intended to delete the element. When finding an element marked as deleted in a NAC match while collecting all rule application labels, this amounts to choosing the first transformation that intended to delete this element and thus resulted in this element being marked. This is similar to FF’s approach of preferring those actions whose preconditions are easier to fulfill. Like the heuristic of FF, our heuristic is not admissible. We can easily create an example domain where our heuristic function counts three graph transformations, e.g., graph transformations that have been applied in parallel to reach the (abstract) goal state in one iteration, although a plan of length two exists, e.g., a plan that requires its two graph transformations to be applied in sequence. In such an example, the overestimation of the costs of reaching a target configuration is essentially caused by the early termination of the successor graph creation loop. Object instantiation The creation of nodes can lead to an explosion of the graph size during the creation of successor graphs in the abstraction. During each iteration of the successor graph creation loop, the size of the next abstract state grows. This is because for each applicable transformation creating one or more nodes, all those nodes are created by the parallel execution of these transformations. Furthermore, each creation of an element results in a new element even if such an element does already exist, possibly even created by the same rule in an earlier iteration. This increases the graph size of each abstract successor state and thus the matching costs. This is also the reason that target graph patterns are likely to have multiple matches in an abstract state, each with a different heuristic value. Such an explosion of the size of a state is not an issue in PDDL-based planners because they do not support object instantiation. An idea to reduce the number of new elements per iteration is to merge all new nodes of the same type into a single node. This, however, affects the propagation of rule application labels. It is not possible anymore to distinctly identify the rule application that was responsible for creating a new node if there was more than one applicable transformation creating a node of the new node’s type. In such a case, we can again prefer those graph transformations whose preconditions are easier to fulfill, i.e., whose LHS matches needed less newly created elements and less graph transformations to create them, similar to FF’s heuristic for selecting achievers. Negative application conditions The equivalent to NACs in PDDL are negative existential quantifications over conjunctive facts. They are usually solved by compiling them away, i.e., translating them into DNF, which results in a blowup of the propositional domain representation, cf. [HN01]. In our approach, we avoid such a blowup by building the support for NACs directly into the abstract planning algorithm. As soon as a graph element marked as 62 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS created or deleted is found within a NAC match, there is no need to check any remaining elements in the same NAC match. We motivated the development of our approach to graph transformation planning by arguing about the need to retain the expressiveness of graph transformation systems when solving graph transformation planning problems and the chances of adapting already known techniques from PDDL-based planning systems. Adapting the idea of FF’s heuristic function, i.e., using the solution length of a relaxed problem as heuristic estimate, is only one of the possibilities. Another possibility that we deem promising is the adaptation of landmark recognition techniques. Alandmark is a literal or a set of literals that occurs in every valid plan. Porteous, Sebastia, and Hoffmann [PSH14] introduced the notion of landmarks in 2001. They identify landmark candidates via a backward search through a relaxed planning graph and verify that they are indeed landmarks by checking whether a relaxed planning graph without those actions achieving a landmark candidate reaches a state satisfying the goal. This approach, which can be performed in polynomial time, is sound but not complete. Since checking whether or not a literal is a landmark is PSPACE-complete, cf. [HPS04], a complete approach is not considered worth the effort. By now, there are several techniques on finding landmarks. The work of Marzal et al. [MSO11] presents a great overview of the most relevant techniques and combines these techniques into one to increase the percentage of landmarks found. When employing a heuristic based on landmarks, it is also important to find useful orderings among landmarks. Landmarks can then be considered as subgoals that have to be reached in sequence to reach the goal. They can either be used to decompose the planning problem into several subproblems, cf. [PSH14], or to derive a heuristic that states how many landmarks still have to be achieved in the correct order. The LAMA planner [RW10a], which won the sequential satisficing track of the 6th International Planning Competition (IPC-2008), uses such a heuristic in a multi-heuristic search, i.e., it alternates between different heuristics, the landmark heuristic and the heuristic of FF, to benefit from both approaches orthogonally. The success of the LAMA planner gave motivation to adapt landmarks-based techniques to graph transformation planning. A first step into this direction was made by Ahmadian [Ahm12], who also developed a predecessor version of our graph transformation planning approach, which uses the length of the parallel relaxed plan as heuristic estimate. He adapted a technique of Zhu and Givan [ZG03], which propagates landmark information through a planning graph via labels. An important aspect of this adaptation concerns the representation of landmarks itself. In propositional state representations, a landmark is a literal. Such a literal can include information about related objects, e.g., a literal with two parameters can express which software component is deployed on which ECU. This is not as easy in graph transformation systems, because it is not possible to rely on the identity of nodes that do not yet exist. Therefore, Ahmadian defined landmarks on the type level. Unfortunately, this makes them imprecise because they do not provide any structural information. A node landmark only states that a node of a certain type has to exist, and an edge landmark only states that an edge of a certain edge type has to 4.6. DISCUSSION 63 exist between two nodes of certain types. An idea to integrate structural information into such landmarks is to consider the combination of multiple edge landmarks involving the same nodes as a landmark on its own. Such a “higher-order” landmark conforms to what is known in related work as a conjunctive landmark, cf. [KRH10]. 5 Durative Graph Transformation Systems This chapter presents a formalism for graph transformations with time in concurrent contexts. This formalism, called durative graph transformation systems (DGTS), provides concepts to specify structural reconfigurations whose execution consumes time as well as dependencies between such reconfigurations. These concepts enable an intuitive specification of temporal reconfigurations on a high level of abstraction. Their formal semantics have been designed such that planning and verification techniques can be applied reasonably. Durative graph transformation systems provide three kinds of rules: durative graph transformation rules,concurrency rules, and urgency rules. From these three kinds of rules, durative graph transformation rules are the most intelligible concept. Syntactically, they are a straightforward extension of ordinary graph transformation rules, i.e., each graph transformation rule is annotated with a natural number representing its execution time. The formal semantics employs a locking mechanism. The idea of this locking mechanism is similar to concurrency control methods implemented by database management systems. Basically, it restricts read or write access to nodes and edges while they are involved in a durative graph transformation. This guarantees that multiple durative graph transformations can not be executed concurrently if they have conflicting needs, cf. [ZH13b] Concurrency rules and urgency rules formalize temporal dependencies between different durative graph transformation rules. The idea for concurrency rules is inspired by the notion of envelope actions [HLF03] in PDDL planning domains. An envelope action is an action whose execution acts as a time window for another action, i.e., the other action requires the envelope action to be applied concurrently. In durative graph transformation systems, we employ concurrency rules to specify such dependencies. In doing so, we allow the envelope to be a disjunction of multiple transformations: there may be multiple durative graph transformations t2 acting as a time window for a durative graph transformation t1 and executing any one of them is sufficient to allow the execution of t1. 65 66 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS The idea of urgency rules is inspired by that of urgent locations, cf. [BDL04], and urgent transitions, cf. [BST99; BT04], both concepts of timed automata. An urgency rule specifies that a certain durative graph transformation t2 has to follow another durative graph transformations t1 urgently, i.e., within a given time frame since the execution of t1finished. Note that the temporal dependencies specified via concurrency and urgency rules appear on the level of transformations, not the level of rules. Consider an example of two robotic arms: one rule implements a robotic arm to continuously rotate an object, another rule specifies a robotic arm to apply adhesive to an object that is continuously being rotated by another robotic arm. In this example, the second rule depends on a concurrent application of the first rule. However, if there are multiple robotic arms and objects, it matters which robotic arm rotates which object. Therefore, a concurrency rule that specifies such a dependency has to include information that defines how the matches of different rules have to relate to each other. The same holds for urgency rules. The formal semantics of all these rules are based on timed graph transformation systems, i.e., any given durative graph transformation system can be translated into a timed graph transformation system. Obviously, instead of specifying a system model as a durative graph transformation systems, a modeler could decide to specify the system model directly as a timed graph transformation systems. However, this would be much less convenient. In the TGTS formalism, the application of rules is timed, but instantaneous, i.e., timed graph transformations do not consume time. Instead, time passes in between two consecutive graph transformations. A durative graph transformation rule could be simulated via two timed graph transformation rules, but this would mean solving a problem manually and repeatedly hat has already been solved by the semantics of durative graph transformation systems. Furthermore, it would require the use of other constructs of timed graph transformation system, i.e., clock instance rules, which enable the measurement of time, and invariant rules, which specify timed conditions. However, the manual handling of clock instances is a tedious duty and can be an error-prone endeavor. Durative graph transformation systems have the advantage that such clock instances are abstracted away and concurrent and urgent behavior are made explicit. Due to being based on timed graph transformation systems, we can make use of the verification procedures for timed graph transformation systems provided by Heinzemann et al. [HE10] and Suck et al. [SHS11]. The approach by Heinzemann et al. [HE10] enables to check whether or not a forbidden graph exists in any state of a timed graph transformation system’s state space, i.e., it is possible to verify CTL formulas of the form EFφ and AG¬φ . In this approach, the absence of a forbidden graph is verified by a backward rule application from the forbidden graph to the start graph. This has previously been done (for untimed graph transformation systems) by Becker et al. [Bec+06] both via an explicit search and the use of symbolic encodings. The approach by Suck et al. [SHS11] introduces a first-order variant of TCTL [ACD93] and enables a verification of first-order TCTL formulas by translating them into TCTL model checking problems for timed automata. 5.1. APPLICATION EXAMPLE: RAILCAB SYSTEM 67 After introducing the running example for this chapter in the next section, the syntax and semantics of durative graph transformation rules is presented in Section 5.2. Being based on timed graph transformation systems, this section also explains the concepts available in the TGTS formalism. For reasons of clarity, the support for negative application conditions is left out for now. Then, Section 5.3 covers how a durative graph transformation correlates with an untimed graph transformation, the termination of durative rules, and possible interleavings among multiple durative rules. The DGTS formalism is extended successively in Section 5.4 to support forbidden edges and forbidden pairs, in Section 5.5 to support concurrency rules, and in Section 5.6 to support urgency rules. Related work in the area of graph transformations with time is covered in Section 5.7. Eventually, Section 5.8 concludes this chapter with a discussion on design decisions regarding the syntax and semantics or concurrency and urgency rules. 5.1 Application Example: RailCab System Each of the three kinds of rules in the DGTS formalism can be motivated with the help of the RailCab system, see Section 1.4, which is why we use a domain of the RailCab system as a running example in this chapter. Instead of providing all rules for the RailCab system at once, we show them as needed, i.e., in introductory paragraphs and syntax sections within the remainder this chapter. Here, we give a general overview on how the RailCab system is modeled. RailCab driving first last Track free Station Convoy driving Publication Base on at partOf member on publisher distributor monitors front next Figure 5.1: Type graph of the RailCab domain Figure 5.1 shows a type graph for the rules in the durative graph transformation system that models the RailCab domain. RailCabs operate on a railway system whose physical structure is specified as part of the system configuration. The railway system consists of track segments that are connected to each other via next edges. A RailCab can occupy one such track segment at a time, which is represented by an on edge to the track segment. Furthermore, RailCabs can coordinate with other RailCabs to form a convoy. Such an active convoy operation is represented in a configuration 68 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS by a node of the Convoy type. A Convoy node has a member edge to each participating RailCab and represents an active instance of the RTCP ConvoyCoordination as well as one instance of the RTCP DistanceControl for each pair of neighboring RailCabs in the convoy. The position of each RailCab in the convoy is given by the first edge, last edge, and front edges in a configuration. Within a convoy, there is a front edge between each pair of neighboring RailCabs. The first and last edge are self edges that represent the head and tail of the convoy. The application scenario mainly consists of reconfigurations to move RailCabs or convoys of RailCabs as well as reconfigurations related to convoy instantiation, deinstantiation, and membership change. Each of these reconfigurations will be specified as a durative graph transformation rule. RailCabs drive slower if they are on their own because driving alone is less energy efficient than driving in a convoy. Therefore, these rules will have different durations. Remember that RailCabs also have to communicate with base stations of the RailCab system. Each RailCab has to be registered at a base station that monitors the track segment that the RailCab occupies. This is represented by an instance of the RTCP Publication. When a RailCab moves from a track segment monitored by one base station to a track segment monitored by another base station, it has to deinstantiate this RTCP and instantiate a new one with the new base station. This change of the RailCab’s registration is a reconfiguration that is required to be executed concurrently to the movement of the RailCab. Therefore, this requirement will be modeled as a concurrency rule. In this application scenario, a RailCab is not allowed to stop abruptly if it is in driving motion. To be allowed to stop, a RailCab first has to brake while still moving to one track segment ahead. Being not allowed to stop abruptly means that there may be no pause between multiple consecutive transformations moving a RailCab; they have to be applied continuously without intermission. Technically, as soon as a reconfiguration that moves a RailCab to another track segment finishes (and the RailCab did not brake during this reconfiguration), another reconfiguration moving this RailCab has to start. This requirement will be specified by means of urgency rules. 5.2 Durative Graph Transformation Rules Adding a notion of durations to graph transformation rules is trivial if the execution of these rules is assumed to be strictly sequential. However, defining a timed semantics for graph transformation rules allowing a concurrent execution is difficult due to the many ways multiple transformations can interact with each other. While unproblematic in some cases, the execution of multiple graph transformation rules simultaneously, i.e., applying them to the same configuration in parallel, can lead to conflicts in other cases. Technically, durative graph transformations can be realized by translating them into two discrete graph transformations that are temporally linked to each other. One graph transformation represents the start of the durative transformation; a 5.2. DURATIVE GRAPH TRANSFORMATION RULES 69 second one represents its end. In doing so, durative graph transformations have application intervals, and as a result, it is possible to apply multiple durative graph transformations concurrently. The question is when to actually perform the reconfiguration that is specified by the durative graph transformation rule. Performing it as part of the discrete graph transformation that represents the start of the durative graph transformation would not be a reasonable solution. The state of the system would be changed long before the durative transformation finished its execution. Therefore, we execute the reconfiguration as part of the second discrete graph transformation. Unfortunately, there might be conflicts between two durative graph transformations if their matches are allowed to overlap arbitrarily. Such a conflict can cause discrete graph transformations representing the end of a durative graph transformation not to be applicable when they are due. Consider a naive approach, which simply uses the application conditions of those discrete graph transformations that represent the start of a durative transformation to decide whether or not multiple durative graph transformations may be applied concurrently. In this case, a discrete graph transformation representing the end of a durative graph transformation might not be applicable when it is due, because other graph transformations that have been applied concurrently may have invalidated its application condition. t1:Track t2:Track t3:Track free t4:Track free r1:RailCab driving r2:RailCab last r3:RailCab first c:Convoy driving next next next on on member member front Figure 5.2: A configuration in the RailCab domain As an example, consider the configuration given in Figure 5.2 and the two graph transformation rules joinConvoy and dissolveConvoy given in Figures 5.3 and 5.4. Each of these rules has only one match in the configuration. The match of joinConvoy maps to the Convoy node c , RailCab nodes r1 and r2 , and Track nodes t1 to t3 , that of dissolveConvoy to Convoy node c , RailCab nodes r2 and r3 , and Track nodes t2 to t4 . Let us assume that one of the two rules, dissolveConvoy , is currently being applied. This means that its condition has already been checked but its actual reconfiguration not yet been executed. Let us further assume that an execution of joinConvoy is scheduled to start while dissolveConvoy is being executed and to end after the execution of dissolveConvoy finished. Since dissolveConvoy ends before 76 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS 5.2.3 Locking Edges and Application Indicators In timed graphs, locking of nodes and edges is done via the creation and deletion of additional edges, called locking edges. Elements of a configuration are locked by applying start rules and unlocked by applying end rules to prevent a concurrent access. There are separate locking edges for reading nodes, reading edges, writing nodes, and writing edges. All these locking edges also have respective edge types in a type graph. To guarantee that the match of an end rule conforms with an earlier match of a start rule, the match of each start rule has to be remembered in a configuration. This is done by adding designated nodes, called application indicators, when applying a start rule. Such an application indicator has an edge to each node in the match of the start rule. These nodes indicate the application scope of the durative rule that induced the start rule. When applying the end rule, we can ensure conformity with the start rule’s match by requiring the same application scope. To properly indicate to which durative rule an application indicator belongs, its type is distinct for each durative rule. All induced rules mentioned earlier are typed via a type graph of the TGTS formalism. This type graph is induced by the type graph of the durative graph transformation system under consideration and contains equivalent types and edge types. In addition to these types and edge types, it needs types and edge types to allow for the creation and deletion of locking edges and application indicators. These types and edge types provide the basis for realizing the locking mechanism and indicating the ongoing application of a durative rule in a configuration. The next paragraphs explain the construction of an induced TGTS type graph via examples, with special attention paid to locking edges and application indicators. Its formal definition is given afterwards. To conveniently refer to locking edge types, we use the functions rlnode :VTG → ETG , wlnode :VTG →ETG , rledge :ETG →ETG , and wledge :ETG →ETG . Each node type nt has two locking edge types, rlnode(nt) and wlnode(nt) , as self edges in the TGTS type graph. For every edge type et that is no locking edge type itself, there are locking edges types rledge(et) and wledge(et) adjacent to the same source and target node types. An example for the inducement of locking edge types is shown in Figure 5.7. In a configuration, an edge of type rlnode(nt) depicts an obtained read lock for a node that has the type nt , and an edge of type wlnode(nt) depicts an obtained write lock. Similarly, an edge of type rledge(et) depicts an obtained read lock for an edge that has the type et, and an edge of type wledge(et)depicts an obtained write lock. Application indicators are used to indicate the ongoing execution of a durative graph transformation in a configuration. Their outgoing edges, called application indicator edges, mark the match of the durative graph transformation rule that has been used, i.e., the subgraph of the configuration that is changed by the transformation. For a durative graph transformation rule with the name name , the node type of the application indicators it instantiates is given by aiType(name) ; the edge type of an edge connecting the application indicator with a node vis given by aiEdgeType(v). 5.2. DURATIVE GRAPH TRANSFORMATION RULES 77 A B x (a) A DGTS type graph A B x wl wl rl rl wl(x) rl(x) (b) Its induced TGTS type graph (incomplete, shows only locking edge types) Figure 5.7: Inducement of locking edge types The induced TGTS type graph shown in Figure 5.7(b) is not yet complete. In addition to locking edges, it contains node types for application indicators: there is a node type for each durative rule and edge types from this node type to every other node type used within the rule, i.e., the TGTS type graph depends on the set of durative rules contained in the durative graph transformation system. Figure 5.8 shows the inducement of a TGTS type graph for a durative graph transformation system containing only a single rule. :A :B :B x«--» x B name := “ExABB” d := 5 (a) A durative rule with the name ExABB and a duration of 5 A B x wl wl rl rl wl(x) rl(x) ExABB underApp1 underApp1 underApp2 (b) An induced TGTS type graph for a DGTS containing only the rule ExABB Figure 5.8: Inducement of a TGTS type graph 78 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS Application indicator edges to different nodes of the same type have to be distinguishable to guarantee that the match of the start rule can be inferred from them. This is important because the end rule of a durative rule is supposed to match the same nodes and edges as its start rule did. If there was no possibility to distinguish application indicator edges, the end rule would still match the correct set of nodes but not necessarily with a correct structure, i.e., it might not necessarily match the correct set of edges. Therefore, application indicator edges to nodes of the same type are individualized with numbers that are distinct within the rule. Consequently, the TGTS type graph contains multiple application indicator edge types from a single application indicator type to a single node type nt if the application indicator’s rule specifies multiple nodes of type nt, see Figure 5.8(b). Now, we give a formal definition for the induced TGTS type graph. Such a type graph is needed by the various kinds of rules of the TGTS formalism. In addition to the types and edge types defined by the DGTS type graph, the induced TGTS type graph provides locking edge types and types for application indicators and its edges. Definition 5.2.8 (Induced TGTS type graph).Let T G be a type graph of a durative graph transformation system. The induced TGTS type graph of T G is a type graph TG where •VTG =VT G ∪VAI, •ETG =ET G ∪EAI ∪ERL.node ∪EWL.node ∪ERL.edge ∪EWL.edge, •|VAI|=|DR| ∧ ∀D ∈ DR :aiType(name)∈VAI, •|EAI|=∑D∈DR |VG,L| ∧ ∀D ∈ DR :∀vt ∈VT G :∃EAI0⊆EAI : |EAI0|=|{v∈VG,L|type(v) = vt}| ∧ src(EAI0) = aiType(name)∧tgt(EAI0) = vt, •|ERL.node|=|VT G | ∧ ∀vt ∈VT G :rlnode(vt)∈ERL.node ∧ src ◦rlnode(vt) = tgt ◦rlnode(vt) = vt, •|EWL.node|=|VT G | ∧ ∀vt ∈VT G :wlnode(vt)∈EWL.node ∧ src ◦wlnode(vt) = tgt ◦wlnode(vt) = vt, •|ERL.edge|=|ET G| ∧ ∀et ∈ET G :rledge(et)∈ERL.edge ∧ src ◦rledge(et) = src(et)∧tgt ◦rledge(et) = tgt(et), and •|EWL.edge|=|ET G| ∧ ∀et ∈ET G :wledge(et)∈EWL.edge ∧ src ◦wledge(et) = src(et)∧tgt ◦wledge(et) = tgt(et). 5.2. DURATIVE GRAPH TRANSFORMATION RULES 79 There is exactly one application indicator for each durative rule, and each node in its LHS has an own application indicator edge type, which connects its type with the application indicator. The latter is so that application indicator edges to different nodes of the same type are distinguishable, which ensures a correct match of the end rule. For each node type, the induced TGTS type graph has two locking edge types as self edges, one for reading and one for writing. There are also two locking edge types for each edge type that is no locking edge type itself. These locking edge types have the same source and target node as the edge type. 5.2.4 Timed Graph Transformation Rules The induced start rule and end rule of a durative graph transformation rule are both defined on top of a timed graph transformation rule. A timed graph transformation rule is similar to an ordinary graph transformation rule, except that it operates on timed graphs instead of ordinary graphs. Finding a match for a timed graph transformation rule works exactly in the same way as finding a match for an ordinary graph transformation rule. In addition to the LHS, RHS, and rule morphism, a timed graph transformation rule specifies a timed guard as well as a set of clock instances to be reset. The time guard is a clock instance constraint that is expressed via clock instances contained in the rule’s LHS. For the rule to be applicable, the time guard has to be evaluated to true. When the rule is applied, those clock instances specified in the set are reset to zero. Definition 5.2.9 (Timed graph transformation rule) . Atimed graph transformation rule tr = (L,R,r,N,z,Vres)consists of • two timed graphs Land R, • an injective rule morphism r:L→R with r(VCI,L) = VCI,R and |VCI,L|= |VCI,R|, • a set of NACs Nwhere each NAC is a tuple (N,n)∈ N with n:L→N, • a clock instance constraint z∈ Z(VCI,L), called time guard, and • a set of clock instances Vres ⊆VCI,R. This timed graph transformation rule is further specialized by the induced start and end rule. Intuitively, the induced start rule serves two purposes. First, it adds information about the execution of the durative rule into the host graph. This is needed for the annotation of time and for the end rule to find a match that corresponds to the match of the start rule. Finding a corresponding match is important because together both rules are supposed to represent the application interval of the durative graph transformation. With a wrong match there would be no meaningful interpretation for the application of a durative rule. Second, it adds locking edges into the host graph such that subsequent rules do not match if they access the same elements in a conflicting manner. 80 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS Definition 5.2.10 (Induced start rule) . Let D= (LD , RD , rD , name , d) be a durative rule. The induced start rule of Dis a timed rule sr = (L,R,r,N,z,Vres)where •VG,L=VLD∧EG,L=ELD, •VG,R=VLD∪ {ai} ∧ type(ai) = aiType(name)∧EG,R=ELD∪ {e|src(e) = ai ∧tgt(e)∈VG,R\ {ai} ∧ type(e) = aiEdgeType ◦tgt(e)} ∪ ERL.node,R∪EWL.node,R∪ERL.edge,R∪EWL.edge,R, •VCI,L=VCI,R=∅∧ECI,L=ECI,R=∅, •iL:LD→Lis the identity morphism on LD∧ris total, •N=NWL.node ∪ NRL.node ∪ NWL.edge ∪ NRL.edge, •z=∅∧Vres =∅, •ERL.node,R={le|∃v∈VG,L:src(le) = tgt(le) = r(v)∧ type(le) = rlnode ◦type(v)}, •EWL.node,R={le|∃v∈VG,L\iL◦dom(rD):src(le) = tgt(le) = r(v)∧ type(le) = wlnode ◦type(v)}, •ERL.edge,R={le|∃e∈EG,L:src(le) = src ◦r(e)∧ tgt(le) = tgt ◦r(e)∧type(le) = rledge ◦type(e)}, •EWL.edge,R={le|∃e∈EG,L\iL◦dom(rD):src(le) = src ◦r(e)∧ tgt(le) = tgt ◦r(e)∧type(le) = wledge ◦type(e)}, •NWL.node ={(N,n)|∃v∈VG,L:VN=VG,L∧ EN=EG,L∪ {ne} ∧ src(ne) = tgt(ne) = n(v)∧ type(ne) = wlnode ◦type(v)∧nis injective}, •NRL.node ={(N,n)|∃v∈VG,L\iL◦dom(rD):VN=VG,L∧ EN=EG,L∪ {ne} ∧ src(ne) = tgt(ne) = n(v)∧ type(ne) = rlnode ◦type(v)∧nis injective}, •NWL.edge ={(N,n)|∃e∈EG,L:VN=VG,L∧ EN=EG,L∪ {ne} ∧ src(ne) = src ◦n(e)∧ tgt(ne) = tgt ◦n(e)∧type(ne) = wledge ◦type(e)∧ nis injective}, and •NRL.edge ={(N,n)|∃e∈EG,L\iL◦dom(rD):VN=VG,L∧ EN=EG,L∪ {ne} ∧ src(ne) = src ◦n(e)∧ tgt(ne) = tgt ◦n(e)∧type(ne) = rledge ◦type(e)∧ nis injective}. The LHS of the induced start rule is the same as the LHS of the durative rule. Its RHS is a copy of the LHS with an additional node ai , which is its application indicator, additional application indicator edges from ai to all other nodes in the RHS, and additional locking edges ERL.node,R , EWL.node,R , ERL.edge,R , and EWL.edge,R . Intuitively, the existence of an application indicator in the host graph indicates the 5.2. DURATIVE GRAPH TRANSFORMATION RULES 81 application of its durative rule, its application indicator edges mark the subgraph that is being changed by the rule application, and locking edges in the host graph indicate whether read or write access to specific nodes and edges is locked. The start rule shall not delete any node or edge. Therefore, the rule morphism r (restricted to graph nodes and edges) is total. According to the definition of a timed graph transformation rule, it is also injective, and as a consequence of its LHS and RHS, unique (up to isomorphism). This allows for a deterministic inducement of start rules. The sets of clock instances, clock instance edges, time guards, and clock instance resets are empty because a start rule does not add a clock instance measuring the execution time itself. Instead, the addition of a clock instance for the execution of a durative rule is done by a clock instance rule, which is presented in Section 5.2.5. The remainder conditions implement the locking functionality. The locking edge sets ERL.node,R and ERL.edge,R specify the creation of a read lock for every required node or edge, respectively. The sets EWL.node,R and EWL.edge,R specify the creation of a write lock for every node or edge that is deleted according to the syntax of the durative rule, i.e., that is not contained in iL◦dom(rD) . The last four sets NWL.node , NRL.node , NWL.edge , and NRL.edge define NACs that are used to check for the existence of locking edges. For each read lock, there is a NAC that forbids the existence of a write lock and vice versa. If the host graph contains parallel edges, the locking mechanism operates more restrictive than necessary. If any one of multiple parallel edges is accessed, this has the effect of locking all those parallel edges. Fortunately, a less restrictive locking of parallel edges can be achieved without changing the semantics: graphs that support parallel edges can simply be simulated by graphs that do not support them, as done in [Bon+07]. Thus, we can preprocess a durative graph transformation system employing parallel edges by mapping it into an equivalent durative graph transformation system without parallel edges. The purpose of the induced end rule is to actually realize the transformation that is syntactically specified by the durative rule and to remove those locking edges that have been created by the start rule. Definition 5.2.11 (Induced end rule) . Let D= (LD , RD , rD , name , d) be a durative rule. The induced end rule of Dis a timed rule er = (L,R,r,N,z,Vres)where •VG,L=VLD∪ {ai} ∧ type(ai) = aiType(name)∧EG,L=ELD∪ {e|src(e) = ai ∧tgt(e)∈VG,L\ {ai} ∧ type(e) = aiEdgeType ◦tgt(e)} ∪ ERL.node,L∪EWL.node,L∪ERL.edge,L∪EWL.edge,L, •VG,R=VRD∧EG,R=ERD, •VCI,L=VCI,R={ci} ∧ ECI,L={(ci,ai)} ∧ ECI,R=∅, •iL:LD→Lis a subgraph isomorphism ∧ iR:RD→Ris the identity morphism on RD∧ r|{VG,L,EG,L}=iR◦rD◦i−1 L∧r|{VCI,L}is total, 82 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS •N=∅, •z={ci ≥d} ∧ Vres =∅, •ERL.node,L={le|∃v∈VG,L:src(le) = tgt(le) = v∧ type(le) = rlnode ◦type(v)}, •EWL.node,L={le|∃v∈VG,L\dom(r):src(le) = tgt(le) = v∧ type(le) = wlnode ◦type(v)}, •ERL.edge,L={le|∃e∈EG,L:src(le) = src(e)∧ tgt(le) = tgt(e)∧type(le) = rledge ◦type(e)}, and •EWL.edge,L={le|∃e∈EG,L\dom(r):src(le) = src(e)∧ tgt(le) = tgt(e)∧type(le) = wledge ◦type(e)}. The LHS of the induced end rule is defined analogously to the RHS of the induced start rule, i.e., it corresponds to the LHS of the durative rule plus an application indicator node, application indicator edges, and locking edges. The RHS of the induced end rule is the same as the RHS of the durative rule. Therefore, the application of the end rule removes the application indicator, the application indicator edges, and the locking edges that were created when the start rule was applied. The rule morphism r is defined in conformity with rD , i.e., the end rule realizes the graph transformation syntactically specified by the durative rule. The end rule also includes a time guard on the value of clock instance ci , which guarantees that the proper amount of time is consumed before the end rule is applied. Note that ci , which is connected via only one edge to ai , is not removed by the end rule. This is because timed graph transformations may neither add nor remove clock instances to or from a timed graph. Adding clock instances is subject to clock instance rules and removing them is subject to a singleton clock instance removal rule. Both are covered in Section 5.2.5. Figure 5.9 shows an example of a durative graph transformation rule and its induced start and end rule. The durative rule is named ExAB and specifies the removal of an edge x during an interval of 5 time units, see Figure 5.9(a). Its induced start rule specifies an application indicator node ExAB to be created, along with two application indicator edges, one to the node of type A and one to the node of type B , see Figure 5.9(b). Here, the target nodes of both application indicator edges are of different type. Therefore, both edges are labeled with underApp1 . If both target nodes were of the same type, one of the application indicator edges would have been labeled with underApp2 instead. Since both of these nodes are preserved in the durative rule, only their read access is locked by an attached creation edge rl in the start rule. For the edge, which is deleted in the durative rule, both its read and write access are locked by attached creation edges rl(x) and wl(x) . Furthermore, forbidden edges allow the application of the start rule only if write access to the preserved nodes and both write and read access to the deletion edge are not locked. The end rule deletes the application indicator node, its adjacent edges, and all locking edges that the start rule creates, see Figure 5.9(c). The application indicator 5.2. DURATIVE GRAPH TRANSFORMATION RULES 83 :A :B «--» x name := “ExAB” d := 5 (a) A durative rule with the name ExAB and a duration of 5 :A :B x wl wl «++» rl «++» rl wl(x) rl(x) «++» rl(x) «++» wl(x) «++» :ExAB «++» underApp1 «++» underApp1 (b) Its induced start rule :A :B «--» x «--» rl «--» rl «--» rl(x) «--» wl(x) «--» :ExAB «--» underApp1 «--» underApp1 ci:Clock «--» hasNode z := {ci ≥5} (c) Its induced end rule Figure 5.9: Inducement of start and end rule edges ensure that the match of the end rule corresponds to the match of the start rule when the end rule is applied. Note that if there were multiple nodes of the same type in the durative rule, the application indicator edges being added to these nodes by the induced start rule would be of different edge types to ensure a correct match for the end rule. The time guard z={ci ≥ 5 } is a condition for the rule’s application. It guarantees that the rule cannot be applied before 5 time units have been passed on the clock instance ci . In the graphical representation, the clock instance the time guard refers to can be identified via its object name. In the formal syntax, we can simply use variable names to make clear to which clock instance a time guard refers 84 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS to. Therefore, we did not define such object names in the syntax of timed graphs or timed graph transformation rules. The time guard only guarantees that the induced end rule is not applied too early. We also need to ensure that it is not applied too late. More precisely, we need to enforce the application of the rule as soon as its time guard is fulfilled. In order to do this, we use invariant rules, which are formally explained in the next section. 5.2.5 Clock Instance and Invariant Rules In Section 5.2.2, we explained that clock instances pertain to parts of a configuration – as opposed to timed automata, where clocks pertain to the complete automaton. Since it is impossible to decide at design time how many clock instances a timed graph transformation system needs, clock instances have to be instantiable. Their instantiation could simply be supported by allowing timed rules to add clock instances; however, the designers of the timed graph transformation formalism decided to put this functionality into separate rules, called clock instance rules. This decision can easily be explained by looking at the implementation of invariants. Invariants are realized as invariant rules in the TGTS formalism. Invariant rules state how long a specific structure is allowed to exist. This structure represents a part of a configuration. It does not matter which transformations resulted in this configuration or whether it is the result of a single or multiple transformations. Since an invariant does not care which timed transformation led to a configuration, why should a clock instance care? By putting the creation and deletion of clock instances into separate rules, the existence of a clock instance in a configuration depends entirely on its structure, not on what happened before. Clock instance rules identify those parts of a configuration that clock instances pertain to. They work similar to timed rules; however, they are specified such that they do not delete anything and create only a single clock instance as well as edges adjacent to this clock instance. To prevent the creation of more than one clock instance to the same part of the configuration, the rule specifies a NAC that is identical to its RHS. Definition 5.2.12 (Clock instance rule) . Aclock instance rule cr = (L , R , r , N) consists of two timed graphs L and R , a rule morphism r:L→R , and a negative application condition (N,n)∈ N where •VG,L=VG,R∧EG,L=EG,R, •VCI,L=∅∧ |VCI,R|=1∧ |ECI,R| ≥ 1, •ris total, and •N=R∧n=r∧ |N | =1. In early variants of the timed graph transformation formalism [Neu07; Hir08], clock instance rules have been derived from timed rules and invariant rules. Later variants, such as [SHS11; Eck+13], also allow their explicit specification. Both variants 5.2. DURATIVE GRAPH TRANSFORMATION RULES 85 are suitable for a semantics of durative rules. Here, we follow the latter approach, i.e., we explicitly define the induced clock instance rule for a given durative rule. An induced clock instance rule has only an application indicator node in its LHS. Therefore, it attaches a clock instance only if a start rule that has been induced by the same durative rule has been applied before. Since the application indicator is typed via the name of the durative rule, there is exactly one induced clock instance rule for each durative rule. Definition 5.2.13 (Induced clock instance rule) . Let D= (LD , RD , rD , name , d) be a durative rule. The induced clock instance rule of Dis a rule cr = (L,R,r,N)where •VG,L=VG,R={ai} ∧ type(ai) = aiType(name)∧EG,L=EG,R=∅and •VCI,L=∅∧ECI,L=∅∧VCI,R={ci} ∧ ECI,R={(ci,ai)}. The operational semantics in Section 5.2.6 is designed such that all applicable clock instance rules are applied immediately after a timed rule has been applied. Upon application, an induced clock instance rule attaches a clock instance to an application indicator node that is not yet connected to a clock instance. Since start rules create application indicator nodes, a clock instance rule creates a clock instance directly after a start rule has been applied. If the part of the configuration that the clock instance pertains to is no longer present, the clock instance needs to be removed as well. This is the case when an end rule is applied because each application of an end rule removes an application indicator. Removing the clock instance is subject to a clock instance removal rule. For a given set of clock instance rules, a clock instance removal rule can be derived automatically. It has a single clock instance as its LHS and an empty RHS. In addition, it specifies the RHSs of all clock instance rules as NACs. As a consequence, the clock instance removal rule deletes a clock instance if the part of the configurations that the clock instance pertains to is no longer present. There is only one clock instance removal rule for the complete timed graph transformation system. Definition 5.2.14 (Clock instance removal rule) . Let CR be a set of clock instance rules. A clock instance removal rule for CR is a rule rrCR = (L,R,r,N)where •VG,L=VG,R=∅∧EG,L=EG,R=∅, •VCI,L={ci} ∧ VCI,R=∅∧ECI,L=ECI,R=∅, •N={(N , n)|∃cr = (Lcr , Rcr , rcr , Ncr)∈CR :N=Rcr ∧n:L→N with n(ci)∈VCI,Rcr }. Invariant rules, which state how long a specific part of a configuration is allowed exist, specify only an LHS. There is no need for an RHS, because invariant rules do not perform transformations. The LHS of an invariant rule contains an arbitrary number of graph node and edges, but exactly one clock instance. They also specify a clock instance constraint. 92 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS p= (LD , RD , rD) and the graph G= (VG , EG) be a projection of D and TiG to the untimed case. If and only if there is a match g:LD→G and a (direct) graph transformation GD,g =⇒H , then there are matches m:Lsr →TiG and x:Ler →TiG0 and transitions hTiG,νisr,m ==⇒ hTiG0,ν0id =⇒ hTiG0,ν00ier,x =⇒ hTiH,νisuch that H= (VH,EH)and TiH = (HTiH,typeTiH)with HTiH = (VH,∅,EH,∅). Proof. Let iG:G→TiG denote the isomorphism between Gand TiG|{VG,EG}. First, we show that, given the match g:LD→G , we can define the matches m:Lsr →TiG and x:Ler →TiG0 such that H=TiH|{VH,EH} . Since Lsr =LD and TiG|{VG,EG}=G hold, we can define m=iG◦g◦i−1 L,sr . Then, we can construct TiG0 and ν0 according to the operational semantics given in Definition 5.2.21. TiG0 now contains one clock instance ci and ν0(ci) = 0. According to Lemma 5.3.1, there is a unique (up to isomorphism) match x:Ler →TiG0 with x◦iL,er =r∗ m◦m◦iL,sr and transitions hTiG0 , ν0id =⇒ hTiG0 , ν00ier,x =⇒ hTiH , νi . Since m=iG◦g◦i−1 L,sr and x◦iL,er =r∗ m◦m◦iL,sr hold, we have x=r∗ m◦iG◦g◦i−1 L,er . Since r∗ m is total, H=TiH|{VH,EH}holds. Second, we show that, given the matches m:Lsr →TiG and x:Ler →TiG0 , we can define the match g:LD→G such that H=TiH|{VH,EH} . Since LD⊆Ler holds, we can define g=i−1 G◦x◦iL,er . Then, we can construct H according to the SPO approach. Since rD=i−1 R,sr ◦rer|{VG,L,EG,L}◦iL,er and g=i−1 G◦x◦iL,er hold, we have H=TiH|{VH,EH}. Intuitively, the resulting graphs H and TiH|{VH,EH} are identical due to three facts. First, executing the start transformation leaves the essential parts of the graph unchanged. Second, all locking edges and special nodes, i.e., application indicators and clock instances, that are created by executing the start transformation are deleted again by executing the end transformation. Third, the end transformation realizes a graph transformation that conforms to the untimed graph transformation – to be precise, their RHSs are the same. 5.3.2 Rule Termination and Interleaving Transition Sequences The application interval of a durative graph transformation is defined by the delay transition that is executed between the application of its induced start and end rule. At an arbitrary point in time during its application interval, an induced start or end rule of another durative rule can be applied. This is intended; otherwise, no concurrent execution would be possible. The question is whether the end rule of an ongoing durative transformation can still be applied if one or more start or end rules induced by other durative rules have been applied during its application interval. The DGTS semantics is designed such that this works, i.e., durative transformations are guaranteed to finish once they have been started. This is formalized in Theorem 5.3.6. 5.3. PROPERTIES OF DURATIVE GRAPH TRANSFORMATION RULES 93 The concurrent application of two durative graph transformation rules means that their induced start and end rules are applied in an interleaving manner. Multiple such interleavings are possible and each such interleaving results in the same configuration. This is formalized in Theorem 5.3.7. Both of these properties build upon some lemmas, which are formalized first. Each of these lemmas gives the sequential or parallel independence between two applications of induced rules. We can then apply the Local Church-Rosser Theorem, see Theorem 2.5.1, which states that two sequential or parallel independent (direct) graph transformations can be applied in any order and both orderings result in the same graph. This is useful when proving Theorems 5.3.6 and 5.3.7. The first lemma considers two induced start rules that are applied in sequence. Lemma 5.3.3 (Sequential independence between two start transformations) . Let D1 and D2 be two durative rules, TiG = (GTiG , typeTiG) a timed graph with GTiG = (VG , VCI , EG , ECI) , and ν a clock instance value assignment such that ν|=TiG . The induced start rules of D1 and D2 are denoted by sr1 and sr2 , respectively. Further, ci1 denotes the clock instance existing during the application interval of D1 and d1 its duration. If there are two action transitions hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i with ν0(ci1) = 0and hTiH1 , ν00isr2,x2 ==⇒ hTiX , ν000i with 0 ≤ν00(ci1)≤d1 , then they are sequentially independent. Proof. We have to show that (i) hTiH1 , ν00isr2,x2 ==⇒ hTiX , ν000i is weakly sequentially independent of hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i and (ii) hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i is weakly parallel independent of hTiG,νisr2,m2 ===⇒ hTiH2,ˆ νi. (i) TiG TiX Lsr1 Rsr1 rsr1 Lsr2 Rsr2 rsr2 TiH1 m1 m∗ 1 r∗ m1 TiH2 m2 m∗ 2 r∗ m2 x2 x∗ 2 r∗ x2 Since there are no application indicators or locking edges in the LHS of sr2 (and thus there are none in the range of x2 ) and hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i creates only such elements, ran(x2)∩TiH1\ran(r∗ m1) = ∅ holds. Thus, we can construct m2:Lsr2→TiG such that r∗ m1◦m2=x2. NACs Furthermore, m2 fulfills each NAC in Nsr2 because hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i does not delete any elements of TiG when deriving TiH1 and x2 already fulfills each NAC in Nsr2by definition. 94 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS (ii) TiG TiX Lsr1 Rsr1 rsr1 Lsr2 Rsr2 rsr2 TiH1 m1 m∗ 1 r∗ m1 TiH2 m2 m∗ 2 r∗ m2 x1 x∗ 1 r∗ x1 Since hTiG , νisr2,m2 ===⇒ hTiH2 , ˆ νi does not delete any elements of TiG when deriving TiH2 , ran(m2)∩TiG \dom(r∗ m1) = ∅ holds. Thus, we can construct x1:Lsr1→TiH2such that x1=r∗ m2◦m1. NACs We show that x1 fulfills each NAC in Nsr1 by contradiction. Let us assume that hTiG , νisr2,m2 ===⇒ hTiH2 , ˆ νi creates locking edges that conflict with a NAC in Nsr1 , i.e., there is a match q1:Nsr1→TiH2 with q1◦nsr1=x1 and (Nsr1,nsr1)∈ Nsr1such that ran(q1)∩TiH2\ran(r∗ m2)6=∅. According to Definition 5.2.10, each NAC that realizes a check for a read lock [write lock] is accompanied by attaching a write lock [read lock] to the same element and vice versa. Thus, hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i creates locking edges that conflict with a NAC of sr2 , i.e., there is a match q2:Nsr2→TiH1 with q2◦nsr2=x2 and (Nsr2 , nsr2)∈ Nsr2 such that ran(q2)∩TiH1\ran(r∗ m1)6=∅ . This is a contradiction to the applicability of hTiH1,ν00isr2,x2 ==⇒ hTiX,ν000i. Intuitively, Lemma 5.3.3 holds due to two facts: 1. The latter start transformation only adds elements to the host graph but deletes none, thus cannot conflict with the applicability of the earlier start transformation. In other words, there cannot be a use-delete conflict. 2. Since no NAC of the latter start transformation matches, i.e., the two transformations are free of produce-forbid conflicts, and the locking mechanism is designed symmetrically, they also have to be free of forbid-produce conflicts. The next lemma considers an end transformation being applied after a start transformation. Instead of “ordinary” sequential independence, it states sequential independence modulo isomorphism. Ordinary sequential independence is not sufficient due to the shared read locks. A locking edge created by the start transformation can be deleted by the end transformation if both transformations read the same element. However, in such a case, there exists another locking edge, which is isomorphic to the first one. Lemma 5.3.4 (Sequential independence modulo isomorphism between a start and an end transformation) . Let D1 and D2 be two durative rules, TiG = (GTiG , typeTiG) a timed graph with GTiG = (VG , VCI , EG , ECI) , and ν a clock instance value assignment such that ν|=TiG and hTiG , νi is reachable from the initial configuration. The induced start rule 5.3. PROPERTIES OF DURATIVE GRAPH TRANSFORMATION RULES 95 of D1 and end rule of D2 are denoted by sr1 and er2 , respectively. Further, ci1 denotes the clock instance existing during the application interval of D1 and d1 its duration. Also, aisr1 and aier2 denote the application indicator in the RHS of sr1 and the LHS of er2 , respectively. If there are two action transitions hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i with ν0(ci1) = 0and hTiH1 , ν00ier2,x2 ==⇒ hTiX , ν000i with 0 ≤ν00(ci1)≤d1 and x2(aier2)6=m∗ 1(aisr1) , then they are sequentially independent modulo isomorphism. Proof. We have to show that (i) hTiH1 , ν00ier2,x2 ==⇒ hTiX , ν000i is weakly sequentially independent modulo isomorphism of hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i and (ii) hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i is weakly parallel independent modulo isomorphism of hTiG , νier2,m2 ===⇒ hTiH2,ˆ νi. (i) TiG TiX Lsr1 Rsr1 rsr1 Ler2 Rer2 rer2 TiH1 m1 m∗ 1 r∗ m1 TiH2 m2 m∗ 2 r∗ m2 x2 x∗ 2 r∗ x2 If hTiH1 , ν00ier2,x2 ==⇒ hTiX , ν000i does not delete any locking edges that have been created by hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i , we have ran(x2)∩TiH1\ran(r∗ m1) = ∅ and can thus construct m2 such that r∗ m1◦m2=x2 . For the case it does, we have to show that m2 can be constructed such that r∗ m1◦m2=e x2 where e x2 is isomorphic to x2. Since x2 is total, there exists an application indicator x2(aier2) in TiG . This application indicator must have been created by the induced start rule sr2 of D2 . Thus, there has to be an application of sr2 in the transition sequence from the initial configuration to TiG . Let y2:Lsr2→TiF denote its match and seq the transition sequence from TiF to TiG. Now we have two cases: either none of the locking edges created by the start rule transformation sr2,y2 ==⇒ has been deleted by any of the transformations in seq or at least one of the locking edges has been deleted. a) None of the locking edges has been deleted by any of the transformations in seq . In this case, we can construct m2 such that r∗ m1◦m2=e x2 where e x2 is isomorphic to x2 because TiG contains locking edges which are isomorphic to the ones created by hTiG,νisr1,m1 ===⇒ hTiH1,ν0i. b) At least one of the locking edges has been deleted by at least one of the transformations in seq . To construct m2 such that r∗ m1◦m2=e x2 where e x2 is isomorphic to x2 , locking edges have to exist that are isomorphic to the locking edges that have been created by sr2,y2 ==⇒ but deleted by a 96 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS transformation in seq . Let ¯ eri denote the rules of transformations deleting the locking edges and ¯ mi:L¯ eri→TiEi their matches with i= 1, . . . , n where nis the number of transformations deleting the locking edges. Each transformation ¯ eri,¯ mi ==⇒ must have been the application of an end rule because start rules do not delete anything. Thus, for each ¯ eri,¯ mi ==⇒ , there must have been a start rule transformation ¯ sri,¯ yi ==⇒ with ¯ yi:L¯ sri→TiDi creating the application indicator that ¯ eri,¯ mi ==⇒ deletes. According to Definitions 5.2.10 and 5.2.11, each ¯ sri,¯ yi ==⇒ also creates locking edges which are isomorphic to the ones that ¯ eri,¯ mi ==⇒deletes. Again we have two cases: either they still exist in TiG or they have been deleted. If they still exist in TiG , we can construct m2 as in (a). If not, they have been deleted by transformations in the transition sequences from TiDi to TiG . In such a case, we can repeat the argument of (b). This argument loop terminates because the sequence of transitions from the initial configuration to TiG is finite. Thus, locking edges exist in TiG that are isomorphic to the ones created by hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i and m2 can be constructed such that r∗ m1◦m2=e x2where e x2is isomorphic to x2. NACs Furthermore, m2|=Ner2 holds obviously because er2 does not contain any NACs. (ii) TiG TiX Lsr1 Rsr1 rsr1 Ler2 Rer2 rer2 TiH1 m1 m∗ 1 r∗ m1 TiH2 m2 m∗ 2 r∗ m2 x1 x∗ 1 r∗ x1 We show that hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i is weakly parallel independent of hTiG , νier2,m2 ===⇒ hTiH2 , ˆ νi . This implies its weak parallel independence modulo isomorphism. We show that the match x1 such that x1=r∗ m2◦m1 can be constructed by contradiction. Let us assume that hTiG , νier2,m2 ===⇒ hTiH2 , ˆ νi deletes elements of TiG which are required for x1to be total, i.e., ran(m1)∩TiG \dom(r∗ m2)6=∅. According to Definition 5.2.11, the deletion of elements is accompanied by releasing a write lock, i.e., deleting a locking edge that constitutes a write operation. Thus, each of the elements in ran(m1)∩TiG \dom(r∗ m2) has a write lock attached. According to Definition 5.2.10, each element in the range of the LHS’s match is accompanied by a NAC that checks for write locks. Since the elements 5.3. PROPERTIES OF DURATIVE GRAPH TRANSFORMATION RULES 97 in ran(m1)∩TiG \dom(r∗ m2) are obviously contained in the range of m1 and these elements have write locks attached, m1 does not fulfill each NAC in Nsr1 . This is a contradiction to the applicability of hTiG,νisr1,m1 ===⇒ hTiH1,ν0i. NACs Furthermore, x1 fulfills each NAC in Nsr1 because hTiG , νier2,m2 ===⇒ hTiH2 , ˆ νi does not create any locking edges when deriving TiH2 , Nsr1 contains only NACs that constitute checks for locking edges, and m1 already fulfills each NAC in Nsr1by definition. Intuitively, Lemma 5.3.4 holds due to two facts: 1. The end transformation consuming locking edges implies the existence of another start transformation that created such locking edges earlier, thus providing exactly the same (up to isomorphism) locking edges as if none of the two transformations were applied. 2. Elements supposed to be deleted by a future end transformation, i.e., the counterpart of the start transformation, cannot be deleted by any other transformation because the start transformation attached locking edges to them. The next lemma considers two end transformations being applicable in the same configuration. For the first two lemmas, we assumed a situation where the transformations are applied in sequence. This ensured their sequential independence. If they were not sequentially independent, the second transformation would not have been applicable at all. When considering two end transformations, this is not necessary. Here, their applicability alone already ensures that they are parallel independent. Lemma 5.3.5 (Parallel independence modulo isomorphism between two end transformations) . Let D1 and D2 be two durative rules, TiG = (GTiG , typeTiG) a timed graph with GTiG = (VG , VCI , EG , ECI) , and ν a clock instance value assignment such that ν|=TiG and hTiG , νi is reachable from the initial configuration. The induced end rules of D1 and D2 are denoted by er1 and er2 , respectively. Further, ci1 and ci2 denote the clock instance existing during the application interval of D1 and D2 , respectively. Also, aier1 and aier2 denote the application indicator in the LHS of er1and er2, respectively. If there are two action transitions hTiG , νier1,m1 ===⇒ hTiH1 , ν0i with ν0(ci1) = 0and hTiG , νier2,m2 ===⇒ hTiH2 , ν00i with ν00(ci2) = 0and m2(aier2)6=m1(aier1) , then they are parallel independent modulo isomorphism. Proof. We have to show that (i) hTiG , νier2,m2 ===⇒ hTiH2 , ν00i is weakly parallel independent modulo isomorphism of hTiG , νier1,m1 ===⇒ hTiH1 , ν0i and (ii) hTiG , νier1,m1 ===⇒ hTiH1 , ν0i is weakly parallel independent modulo isomorphism of hTiG , νier2,m2 ===⇒ hTiH2,ν00i. 98 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS (i) TiG TiX Ler1 Rer1 rer1 Ler2 Rer2 rer2 TiH1 m1 m∗ 1 r∗ m1 TiH2 m2 m∗ 2 r∗ m2 x2 x∗ 2 r∗ x2 If r∗ m1◦m2 is total, i.e., ran(m2)∩TiG \dom(r∗ m1) = ∅ , we can simply construct x2:Ler2→TiH1 such that x2=r∗ m1◦m2 . Otherwise, we have to show that there exist a total morphism e m2:Ler2→TiG such that e m2 is isomorphic to m2 and then construct x2such that x2=r∗ m1◦e m2or there is a contradiction. There are two cases: either ran(m2)∩TiG \dom(r∗ m1) contains only locking elements or it also contains other elements than locks. a) ran(m2)∩TiG \dom(r∗ m1) contains only locking elements. In this case, there exist a e m2:Ler2→TiG which is isomorphic to m2 . Thus, we can construct x2:Ler2→TiH1 such that x2=r∗ m1◦e m2 . The proof that e m2 exists is analogous to the proof of Lemma 5.3.4 (i). b) ran(m2)∩TiG \dom(r∗ m1) contains elements other than locks. According to Definition 5.2.11, the deletion of elements is accompanied by releasing a write lock, i.e., deleting a locking edge that constitutes a write operation. Thus, each of the elements in TiG \dom(r∗ m1)has a write lock attached. These write locks (or isomorphic ones) must have been created by an application of a start rule sr1 of D1 that also created the application indicator that er1,m1 ===⇒ deletes. Similarly, each of the elements in ran(m2) has a read lock attached, which (modulo isomorphism) must have been created by an application of a start rule sr2 of D2 . Let y1:Lsr1→TiF1 and y2:Lsr2→TiF2 denote the the match of sr1 and sr2 , respectively. Since m2(aier2)6=m1(aier1)holds, we have sr16=sr2∨y16=y2. Now, there are two possible orderings: either sr1,y1 ==⇒ happens before or after sr2,y2 ==⇒ in the transition sequence from the initial configuration to TiG . In case of the former, sr1,y1 ==⇒ creates a write lock that still exists in TiF2 . In case of the latter, sr2,y2 ==⇒ creates a read lock that still exists in TiF1 . The existence of these locking elements (or isomorphic ones) can be shown analogously to the argument loop in the proof of Lemma 5.3.4 (i). According to Definition 5.2.10, each creation of a write lock [read lock] is accompanied by a NAC that realizes a check for a read lock [write lock]. Thus, the write lock [read lock] existing in TiF2 [ TiF1 ] conflicts with a NAC of sr2 [ sr1 ]. Both constitute a contradiction to the applicability of the second transformation. 5.3. PROPERTIES OF DURATIVE GRAPH TRANSFORMATION RULES 99 NACs Furthermore, x2|=Ner2 holds obviously because er2 does not contain any NACs. (ii) TiG TiX Ler1 Rer1 rer1 Ler2 Rer2 rer2 TiH1 m1 m∗ 1 r∗ m1 TiH2 m2 m∗ 2 r∗ m2 x1 x∗ 1 r∗ x1 This proof is analogous to the proof of (i). Intuitively, the parallel independence of the end transformations results from the independence of their start transformation counterparts. If the start transformations were not independent, they could not have been applied during the transition sequence from the initial configuration to the current configuration. Now, we formalize the property that ensures that each durative graph transformation terminates properly, i.e., no other transformation can cause the induced end rule of the ongoing durative graph transformation not to be applicable anymore. As a consequence, durative graph transformations can only be executed if they do not interfere with ongoing durative graph transformations. Theorem 5.3.6 (Termination of a durative rule) . Let D1 be a durative rule, TiG = (GTiG , typeTiG) a timed graph with GTiG = (VG , VCI , EG , ECI) , and ν a clock instance value assignment such that ν|=TiG and hTiG , νi is reachable from the initial configuration. The induced start and end rule of D1 are denoted by sr1 and er1 , respectively. Further, iL,sr1 and iL,er1 denote the morphisms identifying the elements of LD1 in Lsr1 and Ler1 , respectively. Also, aisr1 and aier1 denote the application indicator in the RHS of sr1 and the LHS of er2 , respectively. If there exists a transition sequence hTiG , νisr1,m1 ===⇒ hTiH1 , ν0iseq hTiX , ν00i with hTiA , ˆ νier1,a1 ==⇒ hTiB , ˆ ν0i/∈seq for any match a1:Ler1→TiA such that a1(aier1) = r∗ pre ◦ m∗ 1(aisr1) where r∗ pre denotes the derivation morphism of a prefix transition sequence of seq ending in TiA , then there exists a unique (up to isomorphism) match g1:Ler1→TiX such that g1◦iL,er1=r∗ seq ◦r∗ m1◦m1◦iL,sr1 and an action transition hTiX , ν00ier1,g1 ==⇒ hTiY , ν000i . Lsr1Rsr1 TiG TiH1 Ler1Rer1 TiX TiY rsr1 m1m∗ 1 r∗ m1r∗ seq rer1 g1g∗ 1 r∗ g1 Proof. We show this property by induction over the number of transitions in seq. 100 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS Basis step. The transition sequence seq is empty. Thus, hTiH1 , ν0i=hTiX , ν00i holds. Now, we only have to show that there exists a match g1:Ler1→TiH1 such that g1◦iL,er1=r∗ m1◦m1◦iL,sr1 . According to Definitions 5.2.10 and 5.2.11, Ler1=Rsr1 holds. Thus, we can simply define g1 such that g1◦iL,er1=m∗ 1◦rsr1◦ iL,sr1=r∗ m1◦m1◦iL,sr1. Induction step. Let tr2,x2 ==⇒ denote the first transition in seq . That way, we have hTiG , νisr1,m1 ===⇒ hTiH1 , ν0itr2,x2 ==⇒ hTiI , ξiseq0hTiX , ν00i . According to Lemmas 5.3.3 and 5.3.4 the transformations hTiG , νisr1,m1 ===⇒ hTiH1 , ν0itr2,x2 ==⇒ hTiI , ξi are sequentially independent (modulo isomorphism). Theorem 2.5.1 states that sequentially independent transformations can be reordered and still result in the same graph. Thus, we get hTiG , νitr2,m2 ===⇒ hTiH2 , ξ0isr1,x1 ==⇒ hTiI , ξiseq0hTiX , ν00i . Now, we can apply the induction hypothesis, which results in the existence of g1:Ler1→TiX such that g1◦iL,er1=r∗ seq0◦r∗ x1◦x1◦iL,sr1 . Using m1 instead of x1 , we get g1◦iL,er1=r∗ seq0◦r∗ x2◦r∗ m1◦m1◦iL,sr1 . Since r∗ seq =r∗ seq0◦r∗ x2 holds, we get g1◦iL,er1=r∗ seq ◦r∗ m1◦m1◦iL,sr1. While Theorem 5.3.6 ensures that each durative graph transformation terminates properly, even when other transformations are applied during its application interval, it does not state anything about the configuration that results in such cases. The next property does. It states that each interleaving of two durative graph transformations results in the same configuration when both transformations finished (and no other transformation is involved). From a more abstract perspective, this property characterizes all possible interleavings of two durative graph transformations that are independent of each other. Theorem 5.3.7 (Existence of interleaving transition sequences) . Let D1 and D2 be two durative rules, TiG = (GTiG , typeTiG) a timed graph with GTiG = (VG , VCI , EG , ECI) , and ν a clock instance value assignment such that ν|=TiG and hTiG , νi is reachable from the initial configuration. The induced start and end rules of D1 and D2 are denoted by sr1 , er1 , sr2, and er2, respectively. If hTiG , νisr1,m1 ===⇒ hTiH1 , ν0i and hTiG , νisr2,m2 ===⇒ hTiH2 , ν00i are parallel independent, there exist matches ms1 , me1 , ms2 , and me2 for sr1 , er1 , sr2 , and er2 , respectively, such that each of the transition sequences fulfilling the partial order • • sr1,ms1 er1,me1 sr2,ms2 er2,me2 exists and results in the same graph TiZ. 5.3. PROPERTIES OF DURATIVE GRAPH TRANSFORMATION RULES 101 TiG TiH1TiH2 TiI1TiX TiI2 TiY1TiY2 TiZ sr1,m1 sr1,x1 sr1,y1 er1,f1 er1,g1 er1,h1 sr2,m2 sr2,x2 sr2,y2 er2,f2 er2,g2 er2,h2 Proof. According to the Local Church-Rosser Theorem, both sequentializations of two parallel independent transformations result in the same graph. Thus, we have the transition sequence shown in Figure 5.11(a). According to Definitions 5.2.10 and 5.2.11, Ler1=Rsr1 holds. Thus, the match g1:Ler1→TiX can be defined such that g1◦iL,er1=x∗ 1◦rsr1◦iL,sr1=r∗ x1◦x1◦iL,sr1 . The match g2:Ler2→TiX can be defined analogously. Now, we have the transition sequence shown in Figure 5.11(b). According to Lemma 5.3.4, the transformations sr2,x2 ==⇒ and er1,g1 ==⇒ are sequentially independent. Since the Local Church-Rosser Theorem also works for sequentially independent transformations, we get the transition sequence shown in Figure 5.11(c). · · · · · · (a) · · · · · · (b) · · · · · · · · (c) · · · ··· · · · · ? = (d) · · · ··· · · · ? = (e) Figure 5.11: Visual aid for the proof of Theorem 5.3.7 108 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS base station. More precisely, a RailCab has to be registered at a base station that monitors the track segment that the RailCab is currently occupying. The real-time communication between a RailCab and the base station it is registered at is specified by the RTCP Publication, which is represented within configurations and rules as a node of type Pub. When a RailCab moves from a track segment that is monitored by one base station to a track segment that is monitored by another base station, it has to change its publication. This is captured by the durative rule changePublication , which is shown in Figure 5.13. It specifies the revocation of a publication at one base station and the announcement of a publication at another base station. :RailCab:Base :Base «--» :Pub «++» :Pub «++» publisher «++» distributor «--» publisher «--» distributor d := 2 Figure 5.13: Durative rule changePublication A condition for the application of the durative rule changePublication is the concurrent application of another durative rule that moves the RailCab from one track segment to the next. Besides moveRailCab , possible candidates providing such a reconfiguration are moveConvoy and all durative rules related to membership change, e.g., formConvoy or joinConvoy , since they also change the position of RailCabs. All these durative rules are modeled independently from changePublication and their applications exist independently from applications of changePublication. Including the movement of a RailCab in changePublication is not advisable due to two reasons. First, there is more than one reconfiguration that moves a RailCab to the next track segment. A modeler would have to model a separate rule for each such reconfiguration. Second, changing a publication and moving a RailCab are different concerns, and modeling them as one reconfiguration can be considered bad development style. Since reconfigurations addressing different concerns are modeled independently from one another, we need an external means of specifying requirements for their concurrent execution. Concurrency rules provide this means by referencing durative rules and specifying how these rules have to match relatively to one another. 5.5.1 Syntax A concurrency rule specifies a dependency between two sets of durative rules: an application of a durative rule in the first set requires a concurrent application of a durative rule in the second set. Vice versa, the application interval of a durative rule in the second set can be seen as a window of opportunity for rules in the first 5.5. CONCURRENCY RULES 109 set. The involved durative rules of both sets have to match in a certain way for this dependency to be fulfilled. This matching constraint is formalized in the syntax of concurrency rules via two interface graphs and graph morphisms to the involved durative rules. Definition 5.5.1 (Concurrency rule) . Let DR be a set of durative rules. A concurrency rule C= (GT,DT,ST,D,S,name)consists of • a typed graph GT , called connecting graph, with two subgraphs DT and ST , called (concurrency) demander interface and (concurrency) satisfier interface, respectively, • a non-empty set of tuples D , called (concurrency) demander tuples, where each tuple (D , d)∈D references a durative rule D ∈ DR and determines a subgraph of its LHS via an injective morphism d:DT→LD , called (concurrency) demander constraint morphism, • a non-empty set of tuples S , called (concurrency) satisfier tuples, where each tuple (D , s)∈S references a durative rule D ∈ DR and determines a subgraph of its LHS via an injective morphism s:ST→LD , called (concurrency) satisfier constraint morphism, and • a distinct name name. For a durative graph transformation system DS = (T G , GT 0 , DR) with a set of concurrency rules CR, we also write DS = (T G,GT 0,DR,CR). A connecting graph has two dedicated subgraphs, which serve as interfaces for the durative rules involved with a concurrency rule. They are called demander interface and satisfier interface. So-called constraint morphisms from these subgraphs to durative rules define which durative rules fulfill these interfaces and how they have to match relatively to each other. All these constraint morphisms are – together with the rules they map to – contained in the set of demander and satisfier tuples. Each rule referenced by a demander or satisfier tuple fulfills the demander or satisfier interface, respectively. An application of a durative rule referenced by a demander tuple demands a concurrent transformation, and an application of a durative rule referenced by a satisfier tuple satisfies this demand. Therefore, we call a durative rule that is referenced by a demander tuple a demanding rule. If it is referenced by a satisfier tuple, we call it a satisfying rule. The demander and satisfier constraint morphisms constitute matching constraints for all involved durative rules. For a demanding and a satisfying rule to be applicable concurrently, elements contained in the images of their demander and satisfier constraint morphism that originate from the same element in the connecting graph GTalso have to match to the same element in the host graph. Elements that have a preimage in only one of the interface subgraphs DT and ST also restrict the matching: if an element of DT is somehow connected in GT to an element of ST , then the same connection has to exist for their images in the host graph. 110 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS :RailCab:Base :Base «--» :Pub «++» :Pub «++» publish. «++» distri. «--» publish. «--» distri. :RailCab :Track :Track :Base :Base monitors monitors (a) A demander constraint morphism of allowChangePublication to changePublication :RailCab driving :Track +free :Track –free «++» on «--» on next :RailCab :Track :Track :Base :Base monitors monitors (b) A satisfier constraint morphism of allowChangePublication to moveRailCab Figure 5.14: A demander and a satisfier constraint morphism of the concurrency rule allowChangePublication As an example, Figure 5.14 shows a demander and a satisfier constraint morphism for the concurrency rule allowChangePublication . A RailCab is only allowed to change its publication if it is moving from one track segment to the next. Therefore, changePublication is a demanding rule and moveRailCab a satisfying rule. To be precise, changePublication is the only demanding rule, while moveRailCab is one of multiple satisfying rules. All durative rules that move a RailCab from one track segment to the next are valid satisfying rules for allowChangePublication . Here, moveRailCab is exemplary for all satisfying rules of allowChangePublication . The relevant node in this example is the RailCab node, which is why it is contained in both interface subgraphs and thus defined under both demander and satisfier constraint morphisms. However, the fact that the RailCab nodes of both rules have to match the same node in the host graph is not the only matching constraint for the concurrent application of both rules. The new base station also has to monitor the track segment that the RailCab is moving to. This is neither specified in changePublication nor in moveRailCab . It is not specified in changePublication , 5.5. CONCURRENCY RULES 111 because changePublication is not concerned with the movement of RailCabs at all, and it is not specified in moveRailCab , because moveRailCab is not concerned with base stations and publications. Instead, this constraint is expressed via the structure of the connecting graph and both interface subgraphs: each Base node is connected to one of the Track nodes via a monitors edge, and while the Base nodes are contained in the demander interface, the Track nodes are contained in the satisfier interface. For the concurrent application of both rules, this structure also has to exist in the host graph. Note that there can be multiple demander or satisfier constraint morphisms to the same demanding or satisfying rule. If there are multiple demander constraint morphisms to a single demanding rule, this means that the demander interface is fulfilled in multiple different ways, each with a different matching constraint, and an application of this rule causes multiple demands. If there are multiple satisfier constraint morphisms to a single satisfying rule, this means that the satisfier interface can be fulfilled in multiple different ways, i.e., multiple matches can lead to a satisfaction of the demand in concurrent execution. An example for this is the rule formConvoy , which models two RailCabs driving in the same direction. In this rule, a rearward RailCab catches up to a frontward RailCab by covering a distance of two track segments. Figure 5.15 shows two satisfier constraint morphisms mapping to this rule. The first constraint morphism maps the concurrency rule’s RailCab node to the rearward RailCab and the second constraint morphism to the frontward RailCab. Note that the second Track node does not have to be the direct successor of the first Track node for the constraint morphisms to match. When employing concurrency rules in software development, a modeler potentially has to define a lot of demander and satisfier constraint morphisms. While these constraint morphism can be defined conveniently using colors or highlighting, a graphical representation of a concurrency rule involving multiple constraint morphisms, like the ones in Figures 5.14 and 5.15, is rather impractical as an overview because it is not presented coherently in a single diagram. Fortunately, the latter can be done: by employing object names in durative rules, we allow to reference their nodes directly from the connecting graph of a concurrency rule. Figure 5.16 illustrates such a compact representation for the constraint morphisms of Figures 5.14 and 5.15. As an example, consider the RailCab node in the center of the connecting graph. The label #dc::‘rc’ means that the node maps to the node with the object name rc under the constraint morphism dc , which is a demander constraint morphism to the durative rule changePublication . The other three labels define images of this node under the three satisfier constraint morphisms of Figures 5.14(b), 5.15(a) and 5.15(b). 112 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS «++» :Convoy +driving :RailCab –driving +last :RailCab +first :Track +free :Track +free :Track –free next «--» on «++» on «++» member «--» on «++» member next «++» front :RailCab :Track :Track :Base :Base monitors monitors (a) First satisfier constraint morphism of allowChangePublication to formConvoy «++» :Convoy +driving :RailCab –driving +last :RailCab +first :Track +free :Track +free :Track –free next «--» on «++» on «++» member «--» on «++» member next «++» front :RailCab :Track :Track :Base :Base monitors monitors (b) Second satisfier constraint morphism of allowChangePublication to formConvoy Figure 5.15: Two satisfier constraint morphisms of concurrency rule allowChangePublication mapping to the same durative rule 5.5. CONCURRENCY RULES 113 «d/s» :RailCab #dc::‘rc’ #sm::‘rc’ #sf1::‘rc1’ #sf2::‘rc2’ «dem» :Base #dc::‘b1’ «dem» :Base #dc::‘b2’ «sat» :Track #sm::‘t1’ #sf1::‘t1’ #sf2::‘t2’ «sat» :Track #sm::‘t2’ #sf1::‘t3’ #sf2::‘t3’ monitors monitors #dc →dem “changePublication” #sm →sat “moveRailCab” #sf1 →sat “formConvoy” #sf2 →sat “formConvoy” Figure 5.16: Compact representation of demander and satisfier constraint morphisms of Figures 5.14 and 5.15 for concurrency rule allowChangePublication 114 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS 5.5.2 Semantics The semantics of concurrency rules is defined by extending those timed graph transformation rules that have been induced by durative graph transformation rules. This can be seen as modifying the semantics of all durative rules involved in concurrency rules. Each start or end rule whose inducing durative rule is referenced by a concurrency rule is extended. To motivate how these rules are extended, we take a look at their interaction. demanding rule satisfying rule requires concurrent application to have started requires concurrent application to have finished (if existing) sequence of rule applications Figure 5.17: Concurrent execution of a demanding and a satisfying rule Figure 5.17 illustrates the dependency between a demanding and a satisfying rule, e.g., changePublication and moveRailCab . In terms of time, the demanding rule has the “inner” and the satisfying rule the “outer” application interval. The semantics of a concurrency rule extends the induced start and end rules of all involved durative rules such that their application times have to be temporally ordered as in the figure. More precisely, the demanding rule requires the application of the satisfying rule both to have started earlier and to end later. To require the former, we extend the induced rules of both rules such that the demanding transformation checks whether the satisfying transformation is currently being applied. When requiring the latter, we have to make sure that the current satisfying transformation is indeed the same transformation as before. To prevent a second satisfier transformation (of the same or a different rule) from taking the place of the first, we apply a lock and reverse the direction of the dependency, i.e., by checking for potential locks, the satisfying rule guarantees that no demanding transformation is being applied concurrently. Note that a satisfying rule can still be applied independently of a demanding rule, which is why the right arrow in Figure 5.17 has a different meaning than the left. To properly extend the induced rules, we have to be able to check whether a demand in concurrent execution, as specified by a concurrency rule, is satisfied. The satisfaction of such a demand is indicated by a satisfaction indicator, which is a concept that is analogous to an application indicator. Since concurrency rules are not applied in the sense of graph transformations, satisfaction indicators are not created and deleted by concurrency rules but by their referenced satisfying rules. As a consequence of the use of satisfaction indicators, the induced TGTS type graph has to be extended. This extension is made analogously to that of application indicators. The TGTS type graph has to include a type for each satisfaction indicator. For a concurrency rule with the name name , its satisfaction indicator type is given by siType(name) . Furthermore, there has to be a distinct satisfaction indicator edge 5.5. CONCURRENCY RULES 115 type for each node in the satisfier interface of the concurrency rule. For a node v , its satisfaction indicator edge type is given by siEdgeType(v). For a satisfying rule, a satisfaction indicator is simply attached via satisfaction indicator edges to those nodes that are in the range of its satisfier constraint morphism. Unfortunately, the appearance of satisfaction indicators in demanding rules is slightly more complicated than in satisfying rules. Since demander and satisfier constraint morphisms are defined under different subgraphs of the connecting graph, those nodes that the satisfaction indicator has to be attached to do not necessarily exist in a demanding rule’s LHS. Therefore, the LHSs of a demanding rule’s induced start and end rule are extended with those elements in the connecting graph that are not defined under the demander constraint morphism. Technically, this is implemented via a pushout. Adding these elements to the induced rules’ LHSs does not restrict the applicability of the demanding rule. The added elements have to exist in the host graph in either case because the satisfying rule, which is applied concurrently, requires them. Next, we give definitions that state how the induced rules of demanding and satisfying rules are extended. After each definition, we given an example of the extended induced rule. These extensions follow the example of the concurrency rule allowChangePublication with changePublication as demanding rule and moveRailCab as satisfying rule. First, we extend the induced start and end rule of a concurrency demanding rule such that they require the existence of a satisfaction indicator in the host graph. Definition 5.5.2 (Extension of a concurrency demander’s induced start rule) . Let C= (GT , DT , ST , D , S , name) be a concurrency rule and DR a set of durative rules. For each concurrency demander tuple (D , d)∈D , the induced start rule sr = (L , R , r , N , z , Vres) of D ∈ DR is extended into a timed rule sr0= (L0 , R0 , r0 , N0 , z , Vres) where •(Lx,g,i∗), with g:GT→Lxand i∗:L→Lx, is the pushout over d:DT→Land the subgraph isomorphism i:DT→GT, •VSI ={si} ∧ type(si) = siType(name)∧ ESI ={e|src(e) = si ∧tgt(e)∈g(ST)∧ type(e) = siEdgeType ◦g−1◦tgt(e)}, •VG,L0=VG,Lx∪VSI ∧EG,L0=EG,Lx∪ESI, •VG,R0=VG,R∪VSI ∧EG,R0=EG,R∪ESI ∪ERL.node,R0, •VCI,L0=VCI,Lx∧ECI,L0=ECI,Lx∧VCI,R0=VCI,R∧ECI,R0=ECI,R •r0=r∪ {∀x∈Vg(GT\DT)∪Eg(GT\DT):x7→ x} ∪ {si 7→ si} ∪ {∀y∈Vg(ST):(si,y)7→ (si,y)}, and •N0is defined analogously to Definition 5.2.10 such that ∀(N,n)∈ N 0: dom(n) = L0, and •ERL.node,R0={e|src(e) = tgt(e) = si ∧type(e) = rlnode ◦type(si)} 116 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS The pushout adds those elements that are existing in the connecting graph but not in the subgraph constituting the demander interface to the LHS of the extended start rule. This is necessary so that we can attach the satisfaction indicator at its appropriate place. Besides requiring this satisfaction indicator and its satisfaction indicator edges, the extended start rule creates a read lock on the satisfaction indicator. The read lock is used to ensure that the execution of a demanding rule finishes before the execution of a satisfying rule. Apart from that, the extended start rule is almost identical to the original rule. The rule morphism and the NAC morphisms are changed such that they are total on their new domain L0 . This is necessary only for reasons of technical correctness; it does not change their intended purpose. :RailCab +rl :Base +rl :Base +rl «++» :Pub +rl +wl publish. distri. «++» rl(distri.) «++» wl(distri.) «++» rl(publish.) «++» wl(publish.) :Track monitors :Track monitors :SI +rl Figure 5.18: Demanding rule changePublication ’s induced start rule extended according to concurrency rule allowChangePublication Figure 5.18 shows the extended induced start rule of changePublication . The extension was done according to the demander constraint morphism of Figure 5.14(a). For reasons of clarity, the extended rule does not show any NACs or locks that have been generated to support NACs on the level of durative rules. The two Track nodes along with the two monitors edges, which connect the Track nodes to the Base nodes, have been added into the rule by the pushout. Then, the satisfaction indicator is connected to these Track nodes and the only RailCab node. The satisfaction indicator also receives a read lock. Note that the new Track nodes do not have any locks, because they were not present in the original rule. The end rule of a concurrency demanding rule is extended in a similar manner as the start rule. The LHS and RHS include those elements from the connecting graph needed for the satisfaction indicator, the satisfaction indicator itself, and its satisfaction indicator edges. The LHS also includes a read lock on the satisfaction indicator. 5.5. CONCURRENCY RULES 117 Definition 5.5.3 (Extension of a concurrency demander’s induced end rule) . Let C= (GT , DT , ST , D , S , name) be a concurrency rule and DR a set of durative rules. For each concurrency demander tuple (D , d)∈D , the induced end rule er = (L , R , r , N , z , Vres) of D ∈ DR is extended into a timed rule er0= (L0 , R0 , r0 , N , z , Vres) where •(Lx,g,i∗), with g:GT→Lxand i∗:L→Lx, is the pushout over d:DT→Land the subgraph isomorphism i:DT→GT, •VSI ={si} ∧ type(si) = siType(name)∧ ESI ={e|src(e) = si ∧tgt(e)∈g(ST)∧ type(e) = siEdgeType ◦g−1◦tgt(e)}, •VG,L0=VG,Lx∪VSI ∧EG,L0=EG,Lx∪ESI ∪ERL.node,L0, •VG,R0=VG,R∪VSI ∧EG,R0=EG,R∪ESI, •VCI,L0=VCI,Lx∧ECI,L0=ECI,Lx∧VCI,R0=VCI,R∧ECI,R0=ECI,R •r0=r∪ {∀x∈Vg(GT\DT)∪Eg(GT\DT):x7→ x} ∪ {si 7→ si} ∪ {∀y∈Vg(ST):(si,y)7→ (si,y)}, and •ERL.node,L0={e|src(e) = tgt(e) = si ∧type(e) = rlnode ◦type(si)}. Figure 5.19 shows the extended induced end rule of changePublication . Its extension is done analogously to that of the induced start rule in Figure 5.18. :RailCab –rl :Base –rl :Base –rl «--» :Pub –rl –wl «++» :Pub «++» publish. «++» distri. «--» publish. «--» distri. «--» rl(distri.) «--» wl(distri.) «--» rl(publish.) «--» wl(publish.) :Track monitors :Track monitors :SI –rl Figure 5.19: Demanding rule changePublication ’s induced end rule extended according to concurrency rule allowChangePublication The induced rules of a demanding rule require the existence of a satisfaction indicator. The only rules able to create (and delete) this specific satisfaction indicator are induced start (and end) rules of those satisfying rules that are referenced by the same concurrency rule as the demanding rule. 124 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS «d/s» RailCab #dm::‘rc’ #sm::‘rc’ #sb::‘rc’ d/sdriving «d/s» :Track #dm::‘t’ #sm::‘t1’ #sb::‘t1’ «d/s» on #dm →dem “moveRailCab” #sm →sat “moveRailCab” #sb →sat “brakeRailCab” Figure 5.25: Compact representation of demander and satisfier constraint morphisms of Figure 5.24 for urgency rule immediatelyMoveRailCab moveRailCab in Figure 5.24. When referencing the same rule as demanding and satisfying rule, the demander and satisfier constraint morphisms should be different, which is the case here; otherwise, a rule application would satisfy its demand itself. A compact representation for these three constraint morphisms is shown in Figure 5.25. As opposed to the constraint morphisms of the concurrency rule allowChangePublication , for which a compact representation was shown in Figure 5.16, the constraint morphisms here also involve edges. Fortunately, we do not have to state the image of an edge under each constraint morphism. It is sufficient to state which edge is involved in the demander and satisfier interface because the correct source and target nodes of the edge’s image under each constraint morphism can be deduced from the context, i.e., from the connecting graph and the nodes’ images. In the example given here, the demander and satisfier interface are identical. In general, the demander and satisfier interface of urgency rules are, of course, also allowed to be different. An example where they are required to be different might be the release of a driver’s safety belt and the subsequent unlocking of the driver’s door. 5.6.2 Semantics As in concurrency rules, the semantics of urgency rules are defined by extending those start and end rules whose durative rules are referenced by urgency rules. In contrast to concurrency rules, urgency rules also induce new timed rules, invariant rules, and clock instance rules directly. To motivate their purpose, we take an abstract look at how the semantics of an urgency rule is implemented. Figure 5.26 illustrates how the application of a satisfying rule, e.g., brakeRailCab , is enforced by the application of a demanding rule, e.g., moveRailCab . First, the demanding rule indicates a demand in urgent execution. This is done by adding a demand indicator into the host graph. To require that the demand is satisfied, 5.6. URGENCY RULES 125 demanding rule satisfying rule satisfier-firing rule satisfier-cleaning rule requires concurrent application to have started urgent application enforced via invariant rule sequence of rule applications Figure 5.26: Urgent execution of a satisfying rule after a demanding rule i.e., the demand indicator is deleted again, within the time frame specified by the urgency rule, we use an invariant rule over the demand indicator. The only rule able to delete this demand indicator is the timed rule shown above the satisfying rule in Figure 5.26. This rule is called satisfier-firing timed rule. Its application is enforced via the invariant rule. The purpose of the satisfier-firing timed rule is to enforce the application of a satisfying rule. To do so, the rule requires a satisfaction indicator to exist in the host graph. Since the application of the satisfier-firing timed rule is itself enforced via an invariant rule, a compatible satisfaction indicator has to be created before its application. This is what causes a satisfying rule to be applied. Note that a satisfying rule can also be applied when there is no demand in urgent execution. In such a case, the satisfying rule creates a satisfaction indicator that is not deleted by a satisfier-firing timed rule. If left behind in the host graph, a satisfaction indicator might cause a problem when an urgency demanding rule is applied a second time: since the old satisfaction indicator is still available, there is no need for a satisfying rule to be applied. Therefore, satisfaction indicators are deleted by another timed rule, called satisfier-cleaning timed rule. This rule, shown below the satisfying rule in Figure 5.26, has to be applied for every satisfaction indicator in the host graph that is not deleted by an application of the satisfier-firing timed rule. As with the satisfier-firing timed rule, we enforce the application of the satisfier-cleaning timed rule via an invariant rule. The demand and satisfaction indicator can simply be attached to the RHS of the demanding rule and the LHS of the satisfying rule, respectively. Their proper relative positioning in a configuration, i.e., the matching constraints formalized via the demander and satisfier constraint morphisms, is guaranteed by the satisfier-firing timed rule. There is no need to extend the demanding rule with additional nodes and edges as done in the case of concurrency rules. Extending the demanding rule was necessary for concurrency rules because concurrency rules do not have demand indicators. 126 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS The induced TGTS type graph is extended by urgency rules to support their demand and satisfaction indicators. For each demand and satisfaction indicator, it includes a separate type. For an urgency rule with the name name , its demand and satisfaction indicator type are given by diType(name) and siType(name) , respectively. Furthermore, there are distinct demand and satisfaction indicator edge types for each node in the interface subgraphs of the urgency rule. For a node v , its demand and satisfaction indicator edge type are given by diEdgeType(v) and siEdgeType(v) , respectively. Next, we give the formal definitions for the semantics of urgency rules. Between those definitions, we give examples of the extended induced rules and the timed rules directly induced by urgency rules. They follow the example of urgency rule immediatelyMoveRailCab with moveRailCab as demanding rule and brakeRailCab as satisfying rule. First, we extend the induced end rule of an urgency demanding rule such that it creates a demand indicator in the host graph. Definition 5.6.2 (Extension of an urgency demander’s induced end rule) . Let U= (GT , DT , ST , D , S , name , dl) be an urgency rule and DR a set of durative rules. For each urgency demander tuple (D , d)∈D , the induced end rule er = (L , R , r , N , z , Vres) of D ∈ DR is extended into a timed rule er0= (L , R0 , r , N , z , Vres) where •VDI ={di} ∧ type(di) = diType(name)∧ EDI ={e|src(e) = di ∧tgt(e)∈ran(d)∧ type(e) = diEdgeType ◦d−1◦tgt(e)}, •VG,R0=VG,R∪VDI ∧EG,R0=EG,R∪EDI, and •VCI,R0=VCI,R∧ECI,R0=ECI,R. Figure 5.27 shows the extended induced end rule of moveRailCab . This extension is done according to the demander constraint morphism of Figure 5.24(a). As with the last section, the extended rule does not show any NACs or locks that have been :RailCab driving –rl –rl(driving) :Track +free –rl :Track –free –rl –rl(free) –wl(free) «--» on «--» rl(on) «--» wl(on) «++» on next «--» rl(next) «++» :DI Figure 5.27: Demanding rule moveRailCab ’s induced end rule extended according to urgency rule immediatelyMoveRailCab 5.6. URGENCY RULES 127 generated to support NACs on the level of durative rules. The only new element is a demand indicator, which is connected to the RailCab node and the right Track node. To enforce the application of the satisfying rule, the urgency rule induces a satisfier-firing timed rule. Definition 5.6.3 (Induced satisfier-firing timed rule) . Given an urgency rule U= (GT , DT , ST , D , S , name , dl) , the induced satisfier-firing timed rule of U is a timed rule s f tr = (L,R,r,N,z,Vres)where •VDI ={di} ∧ type(di) = diType(name)∧ EDI ={e|src(e) = di ∧tgt(e)∈VDT∧type(e) = diEdgeType ◦tgt(e)}, •VSI ={si} ∧ type(si) = siType(name)∧ ESI ={e|src(e) = si ∧tgt(e)∈VST∧type(e) = siEdgeType ◦tgt(e)}, •VG,L=VGT∪VDI ∪VSI ∧EG,L=EGT∪EDI ∪ESI, •VG,R=VGT∧EG,R=EGT, •VCI,L=VCI,R=∅∧ECI,L=ECI,R=∅, •r:L→R, with dom(r) = R, is the identity morphism on R, •N=∅, and •z=∅∧Vres =∅. The placement of the demand and satisfaction indicator in a satisfier-firing timed rule is determined by the demander and satisfier interface of its inducing urgency rule. This ensures that the satisfying rule is applied at a compatible match, i.e., a match that is compatible with the structure specified in the urgency rule. :RailCab driving :Track on «--» :DI «--» :SI Figure 5.28: Induced satisfier-firing timed rule of urgency rule immediatelyMove- RailCab Figure 5.28 shows the satisfier-firing timed rule that has been directly induced by immediatelyMoveRailCab . It consists of the connecting graph of immediately- MoveRailCab with an additional demand and satisfaction indicator in its LHS. Here, both indicators are connected to both nodes because both interface subgraphs are identical to the connecting graph. 128 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS The application of a satisfier-firing timed rule is coupled to the application of a demanding rule’s induced end rule via a satisfier-firing invariant rule. Note that the interplay between a satisfier-firing timed rule and a satisfier-firing invariant rule is analogous to that of a durative rule’s induced end rule and invariant rule. However, instead of a duration given by a durative rule, this invariant rule specifies a deadline for firing the satisfier-firing timed rule according to the deadline given in the urgency rule. Definition 5.6.4 (Induced satisfier-firing invariant rule) . Given an urgency rule U= (GT , DT , ST , D , S , name , dl) , the induced satisfier-firing invariant rule of U is an invariant rule s f ir = (L,z)where •VG,L={di} ∧ type(di) = diType(name)∧EG,L=∅, •VCI,L={ci} ∧ ECI,L={(ci,di)}, and •z={ci ≤dl}. Both a satisfier-firing timed rule and a satisfier-firing invariant rule need a clock instance to operate on. Such a clock instance is created by a satisfier-firing clock instance rule. Definition 5.6.5 (Induced satisfier-firing clock instance rule) . Given an urgency rule U= (GT , DT , ST , D , S , name , dl) , the induced satisfier-firing clock instance rule of U is a clock instance rule s f cr = (L,R,r,N)where •VG,L=VG,R={di} ∧ type(di) = diType(name)∧EG,L=EG,R=∅and •VCI,L=∅∧ECI,L=∅∧VCI,R={ci} ∧ ECI,R={(ci,di)}. Now, we extend the induced start rule of an urgency satisfying rule such that it creates a satisfaction indicator in the host graph. This extension is done analogously to the extension of the urgency demanding rule’s end rule. Definition 5.6.6 (Extension of an urgency satisfier’s induced start rule) . Let U= (GT , DT , ST , D , S , name) be an urgency rule and DR a set of durative rules. For each urgency satisfier tuple (D , s)∈S , the induced start rule sr = (L , R , r , N , z , Vres) of D ∈ DR is extended into a timed rule sr0= (L,R0,r,N,z,Vres)where •VSI ={si} ∧ type(si) = siType(name)∧ ESI ={e|src(e) = si ∧tgt(e)∈ran(s)∧ type(e) = siEdgeType ◦s−1◦tgt(e)}, •VG,R0=VG,R∪VSI ∧EG,R0=EG,R∪ESI, and •VCI,R0=VCI,R∧ECI,R0=ECI,R. Figure 5.29 shows the extended induced start rule of (urgency) satisfying rule brakeRailCab . The extension is done according to the satisfier constraint morphism of Figure 5.24(c). It is analogous to the extension of the induced end rule of the 5.6. URGENCY RULES 129 :RailCab driving +rl +rl(driving) :Track +rl :Track free +rl +rl(free) +wl(free) on «++» rl(on) «++» wl(on) next «++» rl(next) «++» :SI Figure 5.29: Satisfying rule brakeRailCab ’s induced start rule extended according to urgency rule immediatelyMoveRailCab demanding rule. The only new element is a satisfaction indicator, which is connected to the RailCab node and the left Track node. If the induced start rule of a satisfying rule is applied in a situation where there was no demand in urgent execution, it creates a satisfaction indicator that is not needed and thus not consumed by a satisfier-firing timed rule. To prevent such a satisfaction indicator from remaining in the system until an unrelated satisfier-firing timed rule is applied, we delete it immediately. This is done by a satisfier-cleaning timed rule. Definition 5.6.7 (Induced satisfier-cleaning timed rule) . Given an urgency rule U= (GT , DT , ST , D , S , name) , the induced satisfier-cleaning timed rule of U is a timed rule sctr = (L,R,r,N,z,Vres)where •VSI ={si} ∧ type(si) = siType(name)∧ ESI ={e|src(e) = si ∧tgt(e)∈VST∧type(e) = siEdgeType ◦tgt(e)}, •VG,L=VST∪VSI ∧EG,L=EST∪ESI, •VG,R=VST∧EG,R=EST, •VCI,L=VCI,R=∅∧ECI,L=ECI,R=∅, •r:L→R, with dom(r) = R, is the identity morphism on R, •N=∅, and •z=∅∧Vres =∅. Figure 5.30 shows the satisfier-cleaning timed rule that has been directly induced by immediatelyMoveRailCab . While this rule looks similar to the satisfier-firing timed rule, except for the missing demand indicator, this does not have to be the case for an arbitrary urgency rule. Instead of the complete connecting graph, satisfiercleaning timed rules only use the subgraph constituting the satisfier interface. The demander interface is irrelevant for satisfier-cleaning timed rules, because there was no application of a demanding rule when a satisfier-cleaning timed rule is applied. 130 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS :RailCab driving :Track on «--» :SI Figure 5.30: Induced satisfier-cleaning timed rule of urgency rule immediatelyMove- RailCab The application of a satisfier-cleaning timed rule is coupled to the application of a satisfying rule’s induced start rule via a satisfier-cleaning invariant rule. Definition 5.6.8 (Induced satisfier-cleaning invariant rule) . Given an urgency rule U= (GT , DT , ST , D , S , name) , the induced satisfier-cleaning invariant rule of U is an invariant rule scir = (L,z)where •VG,L={si} ∧ type(si) = siType(name)∧EG,L=∅, •VCI,L={ci} ∧ ECI,L={(ci,si)}, and •z={ci =0}. Both a satisfier-cleaning timed rule and a satisfier-cleaning invariant rule operate on a clock instance that is created by a satisfier-cleaning clock instance rule. Definition 5.6.9 (Induced satisfier-cleaning clock instance rule) . Given an urgency rule U= (GT , DT , ST , D , S , name) , the induced satisfier-cleaning clock instance rule of U is a clock instance rule sccr = (L,R,r,N)where •VG,L=VG,R={si} ∧ type(si) = siType(name)∧EG,L=EG,R=∅and •VCI,L=∅∧ECI,L=∅∧VCI,R={ci} ∧ ECI,R={(ci,si)}. As with a durative graph transformation system without urgency rules, the semantics of a durative graph transformation system with urgency rules is given by its induced timed graph transformation system. Since Definitions 5.2.18 and 5.5.6 do not regard urgency rules, we have to provide a new definition for a durative graph transformation system with urgency rules. Definition 5.6.10 (Induced timed graph transformation system respecting urgency rules) . Let DS = (T G , GT 0 , DR , CR , UR) be a durative graph transformation system that contains a set of concurrency rules CR and a set of urgency rules UR and T S = (TG , TiG0 , TR , IR , CR) its induced timed graph transformation system respecting concurrency rules according to Definition 5.5.6. Its induced timed graph transformation system respecting urgency rules T S0= (TG0 , TiG0 , TR0 , IR0 , CR0) differs from T S in that 5.7. RELATED WORK 131 • the induced TGTS type graph TG has been extended into a type graph TG0 that contains a demand indicator type and a satisfaction indicator type for each urgency rule in UR as well as their demand indicator edge types and satisfaction indicator edge types, • each timed rule tr ∈TR whose inducing durative rule D is referenced by an (urgency) demander or (urgency) satisfier tuple of an urgency rule in UR has been extended into a timed rule tr0∈TR0 as defined in Definitions 5.6.2 and 5.6.6, and if D is referenced by multiple (urgency) demander or (urgency) satisfier tuples (of one or more urgency rules in UR ), then the timed rule is extended successively, and • in addition to the extended variants of those timed rules in TR , the invariant rules in IR , and the clock instance rules in CR , the induced timed graph transformation system T S0 also contains those timed rules, invariant rules, and clock instance rules that have been induced by UR according to Definitions 5.6.3 to 5.6.5 and 5.6.7 to 5.6.9. Note that if there is no compatible satisfying rule that can be applied within the urgency rule’s deadline after the demanding rule’s application (and there is no timed rule making a satisfying rule applicable without passing more time than allowed), a time-stopping deadlock occurs. During operation of the system, this is not a problem per se, because the system does not have to take a path of the state space that leads into a time-stopping deadlock. After all, it is the task of the system’s planning component to find a path leading to a certain goal specification, and if such a path exists, it it obviously free of deadlocks. 5.7 Related Work Gyapay et al. [GHV02] proposed an approach to graph transformation with time that annotates codes with timestamps, called chronos values. Such chronos values can be read and written upon application of a graph transformation rule. When this is done, all written chronos values are set to the same time, i.e., the firing time of the graph transformation, which has to be higher than all chronos values read. Whether or not a node has a chronos value is defined via the type graph, i.e., either all nodes of a certain type have a chronos value or none of them. By assigning chronos values (via the RHS) relatively to their values read (via the LHS), a graph transformation rule can be seen as having some sort of firing duration, although its application is atomic. There are vital differences between graph transformations with time and durative graph transformations. If there are types without chronos values or chronos values of some nodes in the RHS are not updated by a rule application, then there can be nonsensical sequences of graph transformations, where firing times are not monotonically increasing. If not, then no concurrent application of two rules is possible if the matches of both rules overlap. The reason for this is that each rule 132 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS application increases the chronos values of nodes in its match by its firing duration. This is clearly more restrictive than the DGTS formalism. Since graph transformation with time also do not have any concepts analogous to time guard and invariant rules, they would not have been a suitable alternative to TGTS for implementing the various concepts of the DGTS formalism. Syriani and Vangheluwe [SV11; SV08] developed a modular language for timed graph transformation, called MoTif. Its semantics is based on Discrete EVent system Specification (DEVS) [Zei84], where graph are embedded in events being transmitted between scheduling units, called atomic DEVS models, which run in parallel. In MoTif, atomic DEVS models are transformation entities, which can have different execution semantics, e.g., applying a rule once, at all matches, or as many times as possible. These transformation entities have a so-called time advance specifying a delay after which the rule application occurs, i.e., graph transformation rules are applied instantaneously. As with most related approaches, MoTif is more similar to timed graph transformation systems than to durative graph transformation systems. However, a downside compared to the TGTS formalism is that it is not possible to maintain a single consistent representation of the host graph when rules are being applied concurrently, because each transformation entity works on its own copies transmitted via events. As a consequence, concurrency issues are difficult to handle. In the approach of de Lara et al. [Lar+14; Lar+10], graph transformation rules can schedule the application of other graph transformation rules at a later point in time. The approach is based on discrete event simulation, i.e., the application of a graph transformation rule is considered an event, and the scheduling of events is defined in a structure similar to an event graph. This structure contains so-called invocation edges and canceling edges. An invocation edge schedules future rule applications of its target rule when its source rule has been applied. Canceling edges discard scheduled rule applications of their target rules. A scheduled rule application is also discarded when its match is invalidated by another rule application. As a result of this, there is no guarantee that a scheduled rule application will be executed. On the plus side, scheduled rule applications may also include matching constraints. Formally, these matching constraints are defined similar to constraint morphisms in the DGTS formalism. However, there is no connecting graph with individual interface subgraphs. As a consequence, matching constraints can only be formalized via elements existing in both rules. Boronat and Ölveczky [BÖ10] presented MOMENT2, a model transformation framework supporting timed behavior. It is based on Maude [Cla+07], which is a specification language and tool based on rewriting logic and capable of verifying invariants and LTL properties. MOMENT2 introduces several timed constructs: a clock, which increases its value according to the elapsed time, a timed value, which is a clock with a (positive or negative) weighting factor, and a timer, which is a clock running backwards. Timers can be deactivated or reset by graph transformation rules. If a timer reaches zero, time is not allowed to pass anymore, i.e., a graph 5.7. RELATED WORK 133 transformation rule has to be applied before the passing of time may continue. The purpose of timers is thus similar to that of invariant rules in the TGTS formalism. The approach of Rivera et al. [RDV10] is similar to MOMENT2 in that it extends in-place model transformations with timed behavior. In their tool e-Motions, durations of graph transformation rules are specified as intervals representing the minimum and maximum amount of time needed to execute the graph transformation. Its semantics is given by a mapping to Real-Time Maude [ÖM07]. Similar to a durative graph transformation rule in DGTS, a rule in e-Motions is compiled into two rewrite rules, the so-called triggering and realization rule. The use of timers ensures that the amount of time consumed between executing these two rewrite rules satisfies the duration interval. As opposed to MOMENT2, this approach is more high-level because timers do not have to be managed manually. Checking the rule’s applicability is implemented both in the triggering and realization rule. Additional invariant checks are optional, cf. [RVV09]. The rule’s execution is implemented in the realization rule. If the LHS match does not exist anymore when the realization rule is scheduled to be applied, its execution is being canceled. This might lead to erroneous behavior if the execution of a concurrent graph transformation relied on this rule. In the DGTS formalism, such a cancellation of durative rules is prevented by the use of a locking mechanism. A distinguishing feature of e-Motions is the possibility to refer to past and concurrent rule applications, called action executions, in graph transformation rules. As there is no equivalent to a locking mechanism, this feature has to be used by a designer to prevent conflicting graph transformations from being executed concurrently. Using this feature to require a concurrent rule application shares similarities with concurrency rules in the DGTS formalism. However, it is less expressive for three reasons: 1. While the match of a required concurrent rule application can be restricted to contain certain nodes, it is not possible to specify the position of these nodes in the concurrent rule’s LHS. As a result, the concurrency rule allowChangePublication cannot be specified correctly in e-Motions, because its satisfying rule formConvoy has multiple nodes of the RailCab type but only one of them satisfies the demand in concurrent execution. 2. Matching constraints can only be formalized for nodes appearing in both rules. In the DGTS formalism, matching constraints are expressed via the structure of the connecting graph, which enables to relate Base nodes in changePublication to Track nodes in moveRailCab although moveRailCab has no Base nodes and changePublication has no Track nodes. 3. Unlike concurrency rules in the DGTS formalism, it is not possible to specify a disjunction of satisfying concurrent rule applications in e-Motions. Baldan et al. [Bal+08] provide a theoretical framework for the definition of transactional graph transformation systems. A transactional graph transformation systems differentiates between graph elements that are stable and unstable. The stable