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

Abstract

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