Invited Talk: On the Concurrent Semantics of Transformation Systems with Negative Application Conditions

A rich concurrent semantics has been developed along the years for graph transformation systems, often generalizing in non-trivial ways concepts and results fist introduced for Petri nets. Besides the theoretical elegance, the concurrent semantic has potential applications in verification, e.g. in partial order reduction or in the use of finite prefixes of the unfolding for model checking. In practice (graph) transformation systems are often equipped with Negative Application Conditions, that describe forbidden contexts for the application of a rule. The talk will summarize some recent results showing that if the NACs are sufficiently simple (“incremental”) the concurrent semantics lifts smoothly to systems with NACs, but the general case requires original definitions and intuitions. Joint work with Reiko Heckel, Frank Hermann, Susann Gottmann and Nico Nachtigall