Invited Talk: On the Concurrent Semantics of Transformation Systems with Negative Application Conditions Electronic Communications of the EASST Volume 58 (2013) Proceedings of the 12th International Workshop on Graph Transformation and Visual Modeling Techniques (GTVMT 2013) Invited Talk: On the Concurrent Semantics of Transformation Systems with Negative Application Conditions Andrea Corradini 2 pages Guest Editors: Matthias Tichy, Leila Ribeiro Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Invited Talk: On the Concurrent Semantics of Transformation Systems with Negative Application Conditions Andrea Corradini1 1 andrea@di.unipi.it, Dipartimento di Informatica, University of Pisa, Italy Abstract: A rich concurrent semantics has been developed along the years for graph transformation systems, often generalizing in non-trivial ways concepts and results first introduced for Petri nets. Besides the theoretical elegance, the concurrent se- mantics has potential applications in verification and model checking, as witnessed by techniques like partial order reduction or the use of finite, complete prefixes of the unfolding. In practice (graph) transformation systems are often equipped with Negative Appli- cation Conditions (NACs) that describe forbidden contexts for the application of a rule. The use of NACs increases the expressive power of rules, by reducing the num- ber of rules needed to specify a system. In recent years several works addressed the problem of lifting the concurrent semantics developed for transformation systems to the case with NACs [LEOP08, HCEK10]. The talk will summarize some recent results which are the outcome of joint works with Reiko Heckel, Frank Hermann, Susann Gottmann and Nico Nachtigall. Es- sentially, we show that if the NACs are sufficiently simple (incremental) then the concurrent semantics lifts smoothly to systems with NACs, but the general case re- quires original definitions and intuitions. We start discussing the definition of sequential independence for direct derivations with NACs [LEOP08], showing that unlike the plain case, it does not enjoy the fun- damental property of being stable under switching of derivations. The consequence is that sequential independence does not induce a well-defined causal partial order- ing on direct derivations, unless NACs are incremental. As shown in [CHH+12] a possible solution is to transform rules with arbitrary NACs into a set of rules with incremental NACs only. The resulting system is in general an over-approximation of the original one (it can have more derivations), and it can be exploited to identify the really independent direct derivations in the original system. Next a step semantics for transformation systems with NACs is discussed (summa- rizing [CH13]), where several independent rules can be applied simultaneously to the same graph. Unlike the plain case, where the parallel independence of rules guarantees sequentiability in any order, in presence of NACs one should also check that no NAC of one of the rules is generated by any combination of applications of the other rules. If NACs are incremental, though, a static check is sufficient, simply comparing the NACs of each rule with the right-hand sides of the other rules. In this case, it is also shown that canonical derivations exist, that is maximally parallel 1 / 2 Volume 58 (2013) mailto:andrea@di.unipi.it Invited Talk: On the Concurrent Semantics of Transformation Systems with NACs derivations where each rule is applied as early as possible. Finally (deterministic) graph processes for derivations with NACs will be consid- ered. It will be shown that the classical colimit construction that builds a process from a derivation diagram does not work properly with NACs, because isomorphic processes are obtained from derivations that are intuitively not equivalent. The same problem shows up with inhibitor nets, and the solution in the literature consists of enriching the process with some minimal additional information sufficient to dis- tinguish among the non-equivalent derivations that it represents. We will discuss a similar and more general solution for derivations with NACs, suggesting that in the case of incremental NACs the solution coincides with the one proposed for inhibitor nets in [BP99]. Bibliography [BP99] N. Busi, G. M. Pinna. Process Semantics for Place/Transition Nets with Inhibitor and Read Arcs. Fundam. Inform. 40(2-3):165–197, 1999. [CH13] A. Corradini, R. Heckel. Canonical Step Sequences with Negative Application Con- ditions. 2013. Submitted for publication. [CHH+12] A. Corradini, R. Heckel, F. Hermann, S. Gottmann, N. Nachtigall. Transforma- tion Systems with Incremental Negative Application Conditions. In Martı́-Oliet and Palomino (eds.), WADT. Lecture Notes in Computer Science 7841, pp. 127–142. Springer, 2012. [HCEK10] F. Hermann, A. Corradini, H. Ehrig, B. König. Efficient Analysis of Permutation Equivalence of Graph Derivations Based on Petri Nets. ECEASST 29, 2010. [LEOP08] L. Lambers, H. Ehrig, F. Orejas, U. Prange. Parallelism and Concurrency in Ad- hesive High-Level Replacement Systems with Negative Application Conditions. In Ehrig et al. (eds.), Proceedings of the ACCAT workshop at ETAPS 2007. ENTCS 203 / 6, pp. 43–66. Elsevier, 2008. Proc. GTVMT 2013 2 / 2