Model Transformation using Constraint Handling Rules as a basis for Model Interpretation
Marcel Dausend and Frank Raiser. Model Transformation using Constraint Handling Rules as a basis for Model Interpretation. 2011
Abstract:In this paper, we present a model transformation approach aiming to simplify automatic processing of UML state machine models, especially for interpretation. The main requirements are easing the implementation of the interpreter and reducing the number of calculations necessary to execute a model. Our model transformation preserves the semantics and is implemented using CHR. The result of the transformation is an UML state machine model based on the concept of compound transitions. Furthermore we provide an interpreter for those models which supports a comprehensive subset of UML state machine concepts, i. a. junction, fork, join. Our preliminary results show that state machine interpreters can profit from the former model transformation. It simplifies certain aspects of the interpreter implementation and positively affects the performance of the interpreter, e.g. regarding transition selection and transition execution.
Constraint-based hardware synthesis
Andrea Triossi, Salvatore Orlando, Alessandra Raffaetà, Frank Raiser, and Thom Frühwirth. Constraint-based hardware synthesis. 2010, 24th Workshop on (Constraint) Logic Programming
Abstract:We propose a high-level hardware description environment which aims at reducing the gap between application design and the well-established hardware description frameworks. Our motivations rise from an explicit demand for design representation languages at a higher abstraction level with respect to the ones currently adopted by hardware system engineering. A candidate solution can be identied in the constraint programming paradigm. In particular our work investigates the possibility of synthesising special-purpose hardware devices starting from the Constraint Handling Rule formalism. Our method can be used to guide the development of a prototype source-to-source compiler capable of producing, from a constraint based expression, compliant Hardware Description Language code. This paper includes a prototype implementation that allows for ecient parallel execution of multi-set constraint rewrite rules.
Exhaustive parallel rewriting with multiple removals
Frank Raiser and Thom Frühwirth. Exhaustive parallel rewriting with multiple removals. 2010, 24th Workshop on (Constraint) Logic Programming
Abstract:Parallel multiset rewriting is usually restricted to be free of overlaps, such that multiple rule applications cannot remove the same object. In this work, we present a parallel execution strategy for Constraint Handling Rules that allows multiple removals of constraints, for which different multiplicities have no effect on results. We show that the resulting operational semantics is sound with respect to sequential execution and discuss exemplary applications.
Implementing dynamic programming recurrences in constraint handling rules with rule priorities
Ahmed Magdy, Frank Raiser, and Thom Frühwirth. Implementing dynamic programming recurrences in constraint handling rules with rule priorities. 2010, 24th Workshop on (Constraint) Logic Programming
Abstract:Dynamic Programming (DP) is an important technique used in solving optimization problems. A close correspondence between DP recurrences and Constraint Handling Rules with rule priorities (CHRrp) yields natural implementations of DP problems in CHRrp. In this work, we evaluate different implementation techniques with respect to their runtime. From our results we derive a set of guidelines for implementing arbitrary DP problems in CHRrp.
Persistent constraints in constraint handling rules
Hariolf Betz, Frank Raiser, and Thom Frühwirth. Persistent constraints in constraint handling rules. 2010, 23rd Workshop on (Constraint) Logic Programming
Abstract:In the most abstract denition of its operational semantics, the declarative and concurrent programming language CHR is trivially non-terminating for a signicant class of programs. Common refinements of this denition, in closing the gap to real-world implementations, compromise on declarativity and/or concurrency. Building on recent work and the notion of persistent constraints, we introduce an operational semantics avoiding trivial non-termination without compromising on its essential features.
A state equivalence and confluence checker for CHR
Johannes Langbein, Frank Raiser, and Thom Frühwirth. A state equivalence and confluence checker for CHR. 2010, CHR ’10: Proc. 7th Workshop on Constraint Handling Rules
Abstract:Analyzing confluence of CHR programs manually can be an impractical and time consuming task. Based on a new theorem for state equivalence, this work presents the first tool for testing equivalence of CHR states. As state equivalence is an essential component of confluence analysis, we apply this tool in the development of a confluence checker that overcomes limitations of existing checkers. We further provide evaluation results for both tools and detail their modular design, which allows for extensions and reuse in future implementations of CHR tools.
MTSeq – multi-touch-enabled music generation and manipulation based on CHR
Florian Geiselhart, Frank Raiser, Jon Sneyers, and Thom Frühwirth. MTSeq – multi-touch-enabled music generation and manipulation based on CHR. 2010, CHR ’10: Proc. 7th Workshop on Constraint Handling Rules
Abstract:We present MTSeq, an application that combines GUI-driven multi-touch input technology with the CHR-based music generation system APOPCALEAPS and an advanced audio engine. This combination leads to an extended user experience and an intuitive, playful access to the CHR music generation system, and thus introduces CHR to musicians and other non-computer-scientists in an appropriate way. The application is fully modularized and its parts are loosely interconnected through a standard IP networking layer, so it is optionally distributable across multiple machines.
Strong joinability analysis for graph transformation systems in CHR
Frank Raiser and Thom Frühwirth. Strong joinability analysis for graph transformation systems in CHR. 2009, Pre-Proceedings of the 5th International Workshop on Computing with Terms and Graphs (TERMGRAPH), pages 97-112
Abstract:The notion of confluence is prevalent in graph transformation systems (GTS) as well as constraint handling rules (CHR). This work presents a generalized embedding of GTS in CHR that allows to consider strong derivations in confluence analyses. Confluence of a terminating CHR program is decidable, but confluence of a terminating GTS is undecidable. We show that observable confluence in CHR is a sufficient criterion for confluence of the embedded GTS. For this purpose the automatic confluence check for CHR can be reused.
Operational equivalence of graph transformation systems
Frank Raiser and Thom Frühwirth. Operational equivalence of graph transformation systems. 2009, 6th International Workshop on Constraint Handling Rules (CHR), pages 49-62
Abstract:Graph transformation systems (GTS) provide an important theory for numerous applications. With the growing number of GTS-based applications the comparison of operational equivalence of two GTS becomes an important area of research. This work introduces a notion of operational equivalence for graph transformation systems. The embedding of GTS in constraint handling rules (CHR) provides the basis for a decidable and sufficient criterion for operational equivalence of GTS. It is based on the operational equivalence test for CHR programs. A direct application of adapting this test to GTS allows automatic removal of redundant rules.
Equivalence of CHR states revisited
Frank Raiser, Hariolf Betz, and Thom Frühwirth. Equivalence of CHR states revisited. 2009, 6th International Workshop on Constraint Handling Rules (CHR), pages 34-48
Abstract:While it is generally agreed-upon that certain classes of CHR states should be considered equivalent, no standard definition of equivalence has ever been established. Furthermore, the compliance of equivalence with rule application is generally assumed, but has never been proven. We systematically develop an axiomatic notion of state equivalence based on rule applicability and the declarative semantics. We supply the missing proof for its compliance with rule application and provide a proof technique to determine equivalence of given states. The compliance property leads to a simplified formulation of the operational semantics. Furthermore, it justifies a novel view based on equivalence classes of states which provides a powerful proof technique.
Towards Term Rewriting Systems in Constraint Handling Rules
Frank Raiser and Thom Frühwirth. Towards Term Rewriting Systems in Constraint Handling Rules. 2008, Constraint Handling Rules, 5th Workshop, CHR 2008, pages 19-34
Abstract:Term rewriting systems are a formalism in widespread use, often implemented by means of term graph rewriting. In this work we present preliminary results towards an elegant embedding of term graph rewriting in Constraint Handling Rules with rule priorities (CHRrp). As term graph rewriting is well-known to be incomplete with respect to term rewriting, we aim for sound jungle evaluation in CHRrp. Having such an embedding available allows to benet from CHR’s online property and parallelization potential.
On Confluence of Non-terminating CHR Programs
Frank Raiser and Paolo Tacchella. On Confluence of Non-terminating CHR Programs. 2007, Constraint Handling Rules, 4th Workshop, CHR 2007, pages 63-76
Abstract:Confluence is an important property for any kind of rewrite system including CHR, which is a general-purpose declarative committed-choice language consisting of multi-headed guarded rules. CHR can yield a confluence problem, because of non-determinism in the choice of rules using the abstract semantics. Confluence in CHR is an ongoing research topic, because it provides numerous benefits for implementations. However, for non-terminating CHR programs confluence is generally undecidable. In this paper we apply the so-called Strong Church-Rosser property to CHR. This allows determination of confluence for a subset of non-terminating CHR programs.