Showing 1–3 of 3 results for author: Saadat, M G

Encoding Incremental NACs in Safe Graph Grammars using Complementation

Authors: Andrea Corradini, Maryam Ghaffari Saadat, Reiko Heckel

Abstract: In modelling complex systems with graph grammars (GGs), it is convenient to restrict the application of rules using attribute constraints and negative application conditions (NACs). However, having both attributes and NACs in GGs renders the behavioural analysis (e.g. unfolding) of such systems more complicated. We address this issue by an approach to encode NACs using a complementation technique.… ▽ More In modelling complex systems with graph grammars (GGs), it is convenient to restrict the application of rules using attribute constraints and negative application conditions (NACs). However, having both attributes and NACs in GGs renders the behavioural analysis (e.g. unfolding) of such systems more complicated. We address this issue by an approach to encode NACs using a complementation technique. We consider the correctness of our encoding under the assumption that the grammar is safe and NACs are incremental, and outline how this result can be extended to unsafe, attributed grammars. △ Less

Submitted 2 December, 2020; originally announced December 2020.

Comments: In Proceedings GCM 2020, arXiv:2012.01181

ACM Class: Parallelism and concurrency

Journal ref: EPTCS 330, 2020, pp. 88-107

Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototy**

Authors: Nicolas Behr, Reiko Heckel, Maryam Ghaffari Saadat

Abstract: Graph transformation theory relies upon the composition of rules to express the effects of sequences of rules. In practice, graphs are often subject to constraints, ruling out many candidates for composed rules. Focusing on the case of sesqui-pushout (SqPO) semantics, we develop a number of alternative strategies for computing compositions, each theoretically and with an implementation via the Pyt… ▽ More Graph transformation theory relies upon the composition of rules to express the effects of sequences of rules. In practice, graphs are often subject to constraints, ruling out many candidates for composed rules. Focusing on the case of sesqui-pushout (SqPO) semantics, we develop a number of alternative strategies for computing compositions, each theoretically and with an implementation via the Python API of the Z3 theorem prover. The strategies comprise a straightforward generate-and-test strategy based on forbidden graph patterns, a variant with a more implicit logical encoding of the negative constraints, and a modular strategy, where the patterns are decomposed as forbidden relation patterns. For a toy model of polymer formation in organic chemistry, we compare the performance of the three strategies in terms of execution times and memory consumption. △ Less

Submitted 2 December, 2020; v1 submitted 24 March, 2020; originally announced March 2020.

Comments: In Proceedings GCM 2020, arXiv:2012.01181

Journal ref: EPTCS 330, 2020, pp. 126-144

Analysis of Graph Transformation Systems: Native vs Translation-based Techniques

Authors: Reiko Heckel, Leen Lambers, Maryam Ghaffari Saadat

Abstract: The paper summarises the contributions in a session at GCM 2019 presenting and discussing the use of native and translation-based solutions to common analysis problems for Graph Transformation Systems (GTSs). In addition to a comparison of native and translation-based techniques in this area, we explore design choices for the latter, s.a. choice of logic and encoding method, which have a considera… ▽ More The paper summarises the contributions in a session at GCM 2019 presenting and discussing the use of native and translation-based solutions to common analysis problems for Graph Transformation Systems (GTSs). In addition to a comparison of native and translation-based techniques in this area, we explore design choices for the latter, s.a. choice of logic and encoding method, which have a considerable impact on the overall quality and complexity of the analysis. We substantiate our arguments by citing literature on application of theorem provers, model checkers, and SAT/SMT solver in GTSs, and conclude with a general discussion from a software engineering perspective, including comments from the workshop participants, and recommendations on how to investigate important design choices in the future. △ Less

Submitted 19 December, 2019; originally announced December 2019.

Comments: In Proceedings GCM 2019, arXiv:1912.08966

ACM Class: F.4.2

Journal ref: EPTCS 309, 2019, pp. 1-22