Show simple item record

AuthorRaiser, Frankdc.contributor.author
Date of accession2016-03-15T06:22:56Zdc.date.accessioned
Available in OPARU since2016-03-15T06:22:56Zdc.date.available
Year of creation2010dc.date.created
AbstractConstraint Handling Rules (CHR) is a rule- and logic-based formalism and has established itself as an active research topic. In contrast to other rule-based approaches, CHR is both, a theoretical formalism related to first-order and linear-logic, and a practical rule-based programming language. Other rule- and logic-based approaches have been successfully embedded in CHR. For this reason, it is considered a candidate for a lingua-franca of such approaches. We investigate CHR´s suitability for this purpose exemplarily, by considering an embedding of graph transformation systems (GTSs) in CHR, which helps us in identifying points of improvements for strengthening the lingua-franca argument further. In particular, we present a novel formulation of the operational semantics of CHR, which is founded on an equivalence relation over CHR states. It justifies the perspective on CHR as a rule-based rewriting system of equivalence classes, which abstracts over infinitely many possible syntactic variations of a CHR state. Overall, this equivalence-based operational semantics provides a powerful formal analysis tool for CHR, which can significantly reduce proof complexity. The lingua-franca argument implies a potential for cross-fertilization of research. Hence, we revisit program analysis methods available in the CHR literature. Our extended methods apply an invariant to make implicit assumptions explicitly available during analysis, hence, effectively eliminating irrelevant states. The resulting methods are applicable to strictly larger classes of CHR programs and provide more promising approaches towards analyzing more complex programs. Finally, we compare program analysis methods in GTSs and CHR. We find that the adapted CHR confluence test, when applied to a GTS embedded in CHR, corresponds to a sufficient criterion for confluence of the GTS. Similarly, we introduce program equivalence for GTSs with a sufficient criterion based on the CHR program equivalence test.dc.description.abstract
Languageendc.language.iso
PublisherUniversität Ulmdc.publisher
LicenseStandard (Fassung vom 01.10.2008)dc.rights
Link to license texthttps://oparu.uni-ulm.de/xmlui/license_v2dc.rights.uri
KeywordConstraint Handling Rulesdc.subject
KeywordGraph transformation systemsdc.subject
KeywordOperational semanticsdc.subject
KeywordProgram analysisdc.subject
Dewey Decimal GroupDDC 004 / Data processing & computer sciencedc.subject.ddc
LCSHConstraint programming (Computer science)dc.subject.lcsh
TitleGraph transformation systems in Constraint Handling Rules: improved methods for program analysisdc.title
Resource typeDissertationdc.type
DOIhttp://dx.doi.org/10.18725/OPARU-1742dc.identifier.doi
PPN642166080dc.identifier.ppn
URNhttp://nbn-resolving.de/urn:nbn:de:bsz:289-vts-74542dc.identifier.urn
GNDConstraint-Programmierungdc.subject.gnd
GNDProgrammanalysedc.subject.gnd
FacultyFakultät für Ingenieurwissenschaften und Informatikuulm.affiliationGeneral
Date of activation2010-12-03T09:16:03Zuulm.freischaltungVTS
Peer reviewneinuulm.peerReview
Shelfmark print versionZ: J-H 13.847; W: W-H 12.315uulm.shelfmark
DCMI TypeTextuulm.typeDCMI
VTS ID7454uulm.vtsID
CategoryPublikationenuulm.category
Bibliographyuulmuulm.bibliographie


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record