This presentation provides an outlook on the topological approach to spatial and spatio-temporal model checking. We introduce spatial logics, the SLCS language, and its semantics applied to various classes of models: Closure Spaces, Graphs, Polyhedra, and Posets. Additionally, we briefly discuss minimization techniques via the Hennessy-Milner property, and current implementation methods, highlighting relevant tools and applications. Special attention is given to how these techniques are used in practical domains such as imaging and 3D mesh analysis.

Zoom meeting registration link

YouTube live stream

Multilevel modeling extends traditional modeling techniques with a potentially unlimited number of abstraction levels. Multilevel models can be formally represented by multilevel typed graphs whose manipulation and transformation are carried out by multilevel typed graph transformation rules. These rules are cospans of three graphs and two inclusion graph homomorphisms where the three graphs are multilevel typed over a common typing chain. In this paper, we show that typed graph transformations can be appropriately generalized to multilevel typed graph transformations improving preciseness, flexibility and reusability of transformation rules. We identify type compatibility conditions, for rules and their matches, formulated as equations and inequations, respectively, between composed partial typing morphisms. These conditions are crucial presuppositions for the application of a rule for a match—based on a pushout and a final pullback complement construction for the underlying graphs in the category —to always provide a well-defined canonical result in the multilevel typed setting. Moreover, to formalize and analyze multilevel typing as well as to prove the necessary results, in a systematic way, we introduce the category of typing chains and typing chain morphisms.

Zoom meeting registration link

YouTube live stream

We provide a general introduction to the AlgebraicJulia ecosystem and AlgebraicRewriting.jl, which allows for integrating general-purpose code with computation of many graph transformation constructions in a broad variety of categories. Practical applications of graph transformation depend on being able to apply sequences of rewrites in a controlled manner: we present work on a graphical language for the construction and composition of such programs, including computation of normal forms as well as scientific agent-based model simulations. This graphical language can be given semantics in many different contexts (e.g. deterministic, nondeterministic, probabilistic) and can be functorially migrated, which yields graph rewriting programs that operate in other categories.

Zoom meeting registration link

YouTube live stream

Tooling is essential for practical applications in any field. For Graph Transformation, one of the ways to quickly prototype your graph-like domain is by developing a model in GROOVE, a standalone tool that will give you isomorphism checking, state space exploration, and model checking based on a graph grammar consisting of a set of (optionally typed) rules and start graph, optionally complemented with a control program.

In this second part of the tutorials on GROOVE, the following advanced features will be covered: Nested rules, rule parameters, control (functions and recipes), and model checking. Participants are invited to install a local copy of GROOVE and to download the .zip file with examples from the tutorial, which is available on the event's GReTA page.

Zoom meeting registration link

YouTube live stream

In this talk I will present the state of the research on higher-arity algebras from the perspective of (labelled) hypergraph rewriting. Recent discoveries on ternary algebras enabled by the rewriting approach will be discussed and a proposal for computational foundations of formal objects generalizing diagrammatic calculi, such us the one in category theory, will be introduced. This presentation will be done using recently developed function paclets in Mathematica.

Zoom meeting registration link

YouTube live stream

Tooling is essential for practical applications in any field. For Graph Transformation, one of the ways to quickly prototype your graph-like domain is by developing a model in GROOVE, a standalone tool that will give you isomorphism checking, state space exploration and model checking based on a graph grammar consisting of a set of (optionally typed) rules and start graph, optionally complemented with a control program.

In this talk I will show the capabilities of the tool, especially touching on the more advanced features such as nested rules, attribute manipulation, recipes (aka transactions) and various analysis techniques. Some of these are recent extensions. I am also very interested in any type of feedback regarding potential use cases and desirable features.

Zoom meeting registration link

YouTube live stream