arXiv subjects

Frank Raiser

Publications and source records attributed to Frank Raiser.

2 recordsLinked to original sources

arXiv2010

A Complete and Terminating Execution Model for Constraint Handling Rules

We observe that the various formulations of the operational semantics of Constraint Handling Rules proposed over the years fall into a spectrum ranging from the analytical to the pragmatic. While existing analytical formulations facilitate program analysis and formal proofs of program properties, they cannot be implemented as is. We propose a novel operational semantics, which has a strong analytical foundation, while featuring a terminating execution model. We prove its soundness and completeness with respect to existing analytical formulations and we provide an implementation in the form of a source-to-source transformation to CHR with rule priorities.

cs.LO↗

arXiv2010

Analyzing Graph Transformation Systems through Constraint Handling Rules

Graph transformation systems (GTS) and constraint handling rules (CHR) are non-deterministic rule-based state transition systems. CHR is well-known for its powerful confluence and program equivalence analyses, for which we provide the basis in this work to apply them to GTS. We give a sound and complete embedding of GTS in CHR, investigate confluence of an embedded GTS, and provide a program equivalence analysis for GTS via the embedding. The results confirm the suitability of CHR-based program analyses for other formalisms embedded in CHR.

cs.LO↗