Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Purchase individual online access for 1 year to this journal.
Price: EUR 410.00Impact Factor 2024: 0.4
Fundamenta Informaticae is an international journal publishing original research results in all areas of theoretical computer science. Papers are encouraged contributing:
- solutions by mathematical methods of problems emerging in computer science
- solutions of mathematical problems inspired by computer science.
Topics of interest include (but are not restricted to): theory of computing, complexity theory, algorithms and data structures, computational aspects of combinatorics and graph theory, programming language theory, theoretical aspects of programming languages, computer-aided verification, computer science logic, database theory, logic programming, automated deduction, formal languages and automata theory, concurrency and distributed computing, cryptography and security, theoretical issues in artificial intelligence, machine learning, pattern recognition, algorithmic game theory, bioinformatics and computational biology, quantum computing, probabilistic methods, & algebraic and categorical methods.
Authors: Rensink, Arend | Rozenberg, Grzegorz | Schürr, Andy
Article Type: Other
DOI: 10.3233/FI-2012-703
Citation: Fundamenta Informaticae, vol. 118, no. 1-2, pp. v-vii, 2012
Authors: Heindel, Tobias
Article Type: Research Article
Abstract: The introduction of adhesive categories revived interest in the study of properties of pushouts with respect to pullbacks that started over thirty years ago for the category of graphs. Adhesive categories – of which graphs are the “archetypal” example – are defined by a single property of pushouts along monos that implies essential lemmas and central theorems of double pushout rewriting such as the local Church-Rosser Theorem. The present paper shows that a strictly weaker condition on pushouts suffices to obtain essentially the same results: it suffices to require pushouts to be hereditary, i.e. they have to remain pushouts when …they are embedded into the associated category of partial maps. This fact however is not the only reason to introduce partial map adhesive categories as categories with pushouts along monos (of a certain stable class) that are hereditary. There are two equally important motivations: first, there is an application relevant example category that cannot be captured by the more established variations of adhesive categories; second, partial map adhesive categories are “conceptually similar” to adhesive categories as the latter can be characterized as those categories with pushout along monos that remain bi-pushouts when they are embedded into the associated bi-category of spans. Thus, adhesivity with partial maps instead of spans appears to be a natural candidate for a general rewriting framework. Show more
Keywords: graph transformation, category theory, adhesive categories, double pushout rewriting, single pushout rewriting
DOI: 10.3233/FI-2012-704
Citation: Fundamenta Informaticae, vol. 118, no. 1-2, pp. 1-33, 2012
Authors: Ehrig, Hartmut | Golas, Ulrike | Habel, Annegret | Lambers, Leen | Orejas, Fernando
Article Type: Research Article
Abstract: Graph transformation systems have been studied extensively and applied to several areas of computer science like formal language theory, the modeling of databases, concurrent or distributed systems, and visual, logical, and functional programming. In most kinds of applications it is necessary to have the possibility of restricting the applicability of rules. This is usually done by means of application conditions. In this paper, we continue the work of extending the fundamental theory of graph transformation to the case where rules may use arbitrary (nested) application conditions. More precisely, we generalize the Embedding theorem, and we study how local confluence can …be checked in this context. In particular, we define a new notion of critical pair which allows us to formulate and prove a Local Confluence Theorem for the general case of rules with nested application conditions. All our results are presented, not for a specific class of graphs, but for any arbitrary ℳ-adhesive category, which means that our results apply to most kinds of graphical structures. We demonstrate our theory on the modeling of an elevator control by a typed graph transformation system with positive and negative application conditions. Show more
Keywords: ℳ-adhesive transformation systems, ℳ-adhesive categories, graph replacement categories, nested application conditions, embedding, critical pairs, local confluence
DOI: 10.3233/FI-2012-705
Citation: Fundamenta Informaticae, vol. 118, no. 1-2, pp. 35-63, 2012
Authors: Orejas, Fernando | Lambers, Leen
Article Type: Research Article
Abstract: Applying an attributed graph transformation rule to a given object graph always implies some kind of constraint solving. In many cases, the given constraints are almost trivial to solve. For instance, this is the case when a rule describes a transformation G ⇒ H, where the attributes of H are obtained by some simple computation from the attributes of G. However there are many other cases where the constraints to solve may be not so trivial and, moreover, may have several answers. This is the case, for instance, when the transformation process includes some kind of searching. In the current …approaches to attributed graph transformation these constraints must be completely solved when defining the matching of the given transformation rule. This kind of early binding is well-known from other areas of Computer Science to be inadequate. For instance, the solution chosen for the constraints associated to a given transformation step may be not fully adequate, meaning that later, in the search for a better solution, we may need to backtrack this transformation step. In this paper, based on our previous work on the use of symbolic graphs to deal with different aspects related with attributed graphs, including attributed graph transformation, we present a new approach that, based on the new notion of narrowing graph transformation rule, allows us to delay constraint solving when doing attributed graph transformation, in a way that resembles lazy computation. For this reason, we have called lazy this new kind of transformation. Moreover, we show that the approach is sound and complete with respect to standard attributed graph transformation. A running example, where a graph transformation system describes some basic operations of a travel agency, shows the practical interest of the approach. Show more
Keywords: Attributed graph transformation, symbolic graph transformation, lazy transformation
DOI: 10.3233/FI-2012-706
Citation: Fundamenta Informaticae, vol. 118, no. 1-2, pp. 65-96, 2012
Authors: Jurack, Stefan | Taentzer, Gabriele
Article Type: Research Article
Abstract: Model-driven development (MDD) has become a promising trend in software engineering. The model-driven development of highly complex software systems may lead to large models which deserve a modularization concept to enable their structured development in larger teams. Graphs are a natural way to represent the underlying structure of visual models. Typed graphs with inheritance and containment structures are well suited to describe the essentials of models based on the Eclipse Modeling Framework (EMF). Composite graphs can specify the logical distribution of EMF models and therefore, can form the conceptual basis for composite modeling in model-driven development. This is done based …on the formal foundation of distributed graphs. Moreover, this category-theoretical foundation allows for the precise definition of consistent composite graph transformations satisfying all inheritance and containment conditions. Show more
Keywords: graph transformation, distributed graph, composite modeling, model-driven development
DOI: 10.3233/FI-2012-707
Citation: Fundamenta Informaticae, vol. 118, no. 1-2, pp. 97-134, 2012
Authors: Poskitt, Christopher M. | Plump, Detlef
Article Type: Research Article
Abstract: GP (for Graph Programs) is an experimental nondeterministic programming language for solving problems on graphs and graph-like structures. The language is based on graph transformation rules, allowing visual programming at a high level of abstraction. In particular, GP frees programmers from dealing with low-level data structures. In this paper, we present a Hoare-style proof system for verifying the partial correctness of (a subset of) graph programs. The pre- and post-conditions of the calculus are nested graph conditions with expressions, a formalism for specifying both structural graph properties and properties of labels. We show that our proof system is sound with …respect to GP's operational semantics and give examples of its use. Show more
DOI: 10.3233/FI-2012-708
Citation: Fundamenta Informaticae, vol. 118, no. 1-2, pp. 135-175, 2012
Authors: Gadducci, Fabio | Lafuente, Alberto Lluch | Vandin, Andrea
Article Type: Research Article
Abstract: Quantified μ-calculi combine the fix-point and modal operators of temporal logics with (existential and universal) quantifiers, and they allow for reasoning about the possible behaviour of individual components within a software system. In this paper we introduce a novel approach to the semantics of such calculi: we consider a sort of labeled transition systems called counterpart models as semantic domain, where states are algebras and transitions are defined by counterpart relations (a family of partial homomorphisms) between states. Then, formulae are interpreted over sets of state assignments (families of partial substitutions, associating formula variables to state components). Our proposal allows …us to model and reason about the creation and deletion of components, as well as the merging of components. Moreover, it avoids the limitations of existing approaches, usually enforcing restrictions of the transition relation: the resulting semantics is a streamlined and intuitively appealing one, yet it is general enough to cover most of the alternative proposals we are aware of. The paper is rounded up with some considerations about expressiveness and decidability aspects. Show more
Keywords: Quantified μ-calculi, counterpart semantics, modal logics, graph transformation
DOI: 10.3233/FI-2012-709
Citation: Fundamenta Informaticae, vol. 118, no. 1-2, pp. 177-205, 2012
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl