References of "Mathematical Structures in Computer Science"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailValidating Brouwer's Continuity Principle for Numbers Using Named Exceptions
Rahli, Vincent UL; Bickford, Mark

in Mathematical Structures in Computer Science (2017)

Detailed reference viewed: 61 (2 UL)
Full Text
Peer Reviewed
See detailFormal Analysis of Model Transformations Based on Triple Graph Grammars
Hermann, Frank UL; Ehrig, Hartmut; Golas, Ulrike et al

in Mathematical Structures in Computer Science (2014), 24(4-08), 1-57

Triple graph grammars (TGGs) are a well-established concept for the specification and execution of bidirectional model transformations within model driven software engineering. Their main advantage is an ... [more ▼]

Triple graph grammars (TGGs) are a well-established concept for the specification and execution of bidirectional model transformations within model driven software engineering. Their main advantage is an automatic generation of operational rules for forward and backward model transformations, which simplifies specification and enhances usability as well as consistency. In this paper we present several important results for analysing model transformations based on the formal categorical foundation of TGGs within the framework of attributed graph transformation systems. Our first main result shows that the crucial properties of correctness and completeness are ensured for model transformations. In order to analyse functional behaviour, we generate a new kind of operational rule, called a forward translation rule. We apply existing results for the analysis of local confluence for attributed graph transformation systems. As additional main results, we provide sufficient criteria for the verification of functional behaviour as well as a necessary and sufficient condition for strong functional behaviour. In fact, these conditions imply polynomial complexity for the execution of the model transformation. We also analyse information and complete information preservation of model transformations, that is, whether a source model can be reconstructed (uniquely) from the target model computed by the model transformation. We illustrate the results for the well-known model transformation example from class diagrams to relational database models. [less ▲]

Detailed reference viewed: 53 (5 UL)
Full Text
Peer Reviewed
See detailAnalysis of Permutation Equivalence in M-adhesive Transformation Systems with Negative Application Conditions
Hermann, Frank UL; Ehrig, Hartmut; Corradini, Andrea

in Mathematical Structures in Computer Science (2014), 24(4-09), 1-47

M-adhesive categories provide an abstract framework for a large variety of specification frameworks for modelling distributed and concurrent systems. They extend the well-known frameworks of adhesive and ... [more ▼]

M-adhesive categories provide an abstract framework for a large variety of specification frameworks for modelling distributed and concurrent systems. They extend the well-known frameworks of adhesive and weak adhesive HLR categories and integrate high-level constructs such as attribution as in the case of typed attributed graphs. In the current paper, we investigate -adhesive transformation systems including negative application conditions (NACs) for transformation rules, which are often used in applications. For such systems, we propose an original equivalence on transformation sequences, called permutation equivalence, that is coarser than the classical switch equivalence. We also present a general construction of deterministic processes for -adhesive transformation systems based on subobject transformation systems. As a main result, we show that the process obtained from a transformation sequence identifies its equivalence class of permutation-equivalent transformation sequences. Moreover, we show how the analysis of this process can be reduced to the analysis of the reachability graph of a generated Place/Transition Petri net. This net encodes the dependencies between rule applications of the transformation sequence, including the inhibiting effects of the NACs. [less ▲]

Detailed reference viewed: 57 (10 UL)