## PublicationsAbstractPublications of Iovka Boneva by topic and with abstracts. Find also a condensed list of all publications. - Security and updates in XML databases
- Logic and tree automata for semi-structured databases
- Graphs for object oriented verification
- Process algebra
- Doctorate thesis
## Security and updates in XML databases## View update translation for XMLIn ICDT 2011. We study the problem of update translation for views on XML documents. More precisely, given an XML view definition and a user defined view update program, find a source update program that translates the view update without side effects on the view. Additionally, we require the translation to be defined on all possible source documents; this corresponds to Hegner's notion of uniform translation. The existence of such translation would allow to update XML views without the need of materialization.
The class of views we consider can remove parts of the document and rename nodes. Our update programs define the simultaneous application of a collection of atomic update operations among insertion/deletion of a subtree and node renaming. Such update programs are compatible with the XQuery Update Facility (XQUF) snapshot semantics. Both views and update programs are represented by recognizable tree languages. We present as a proof of concept a small fragment of XQUF that can be expressed by our update programs, thus allows for update propagation. Two settings for the update problem are studied: without source constraints, where all source updates are allowed, and with source constraints, where there is a restricted set of authorized source updates. Using tree automata techniques, we establish that without constraints, all view updates are uniformly translatable and the translation is tractable. In presence of constraints, not all view updates are uniformly translatable. However, we introduce a reasonable restriction on update programs for which uniform translation with constraints becomes possible. ## The View Update Problem for XMLIn EDBT/ICDT Workshops (Updates in XML), March 2010, Lausanne, Switzerland We study the problem of update propagation across views in the setting where both the view and the source database are XML documents. We consider a simple class of XML views that remove selected parts of the source document. The considered update operations permit to insert and delete subtrees of the document. We focus on constructing propagations that are 1) schema compliant i.e., when applied to the source document they give a document that satisfies the document schema; 2) side-effect free i.e., the view of the new source document is exactly as the result of applying the user update to the old view. We present a special structure allowing to capture all such propagations. We also show how to use this structure to capture only those propagations that affect minimally the parts of the document which are not visible in the view. Finally, we present a general outline of a polynomial algorithm constructing a unique propagation.
## Logic and tree automata for semi-structured databases## Expressiveness of a spatial logic for treesIn 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005) IEEE Comp. Soc. Press, 2005. With Jean-Marc Talbot and Sophie Tison. We investigate the quantifier-free fragment of the TQL logic proposed by Cardelli and Ghelli. The TQL logic, inspired from the ambient logic, is the core of a query language for semistructured data represented as unranked and unordered trees. The fragment we consider here, named STL, contains as main features spatial composition and location as well as a fixed point construct.
We prove that satisfiability for STL is undecidable.We show also that STL is strictly more expressive that the Presburger monadic second-order logic (PMSO) of Seidl, Schwentick and Muscholl when interpreted over unranked and unordered edge-labeled trees. We define a class of tree automata whose transitions are conditioned by arithmetical constraints; we show then how to compute from a closed STL formula a tree automaton accepting precisely the models of the formula. Finally, still using our tree automata framework, we exhibit some syntactic restrictions over STL formulae that allow us to capture precisely the logics MSO and PMSO.
## Automata and Logics for Unranked and Unordered TreesIn 20th International Conference on Rewriting Techniques and Applications (RTA 2005). Lecture Notes in Computer Science (3467). Springer Verlag, 2005. With Jean-Marc Talbot. In this paper, we consider the monadic second order logic (MSO) and two of its extensions, namely Counting MSO (CMSO) and Presburger MSO (PMSO), interpreted over unranked and unordered trees. The last two logics were already associated with some notions of tree automata: for a logical sentence, one can build a tree automaton whose accepted language is precisely the models of this sentence. However, for CMSO and PMSO, the respective associated automata are quite different. For CMSO, tree automata come from the notion of algebraic recognizability; for PMSO, a new class of automata, namely Presburger tree automata (PTA), is tailored: these are tree automata whose transitions are arithmetical constraints. We show in this paper that those different notions of tree automata can be adapted to the three logics we consider: first, for MSO and CMSO, we define an equivalent class of tree automata as syntactic restriction of Presburger tree automata. This allows us to establish that MSO-CMSO-PMSO is a strict increasing hierarchy over unranked and unordered trees. We also make a parallel between PTA (and their restrictions) and a class of tree automata inspired from hedge automata. Secondly, we show how a purely algebraic notion of recognizability can be proposed for MSO and PMSO. Finally, we show that PMSO-definable tree languages are exactly the equational tree languages.
## On Complexity of Model-Checking for the TQL LogicIn TC1 3rd IFIP International Conference on Theoretical Computer Science (TCS2004). Kluwer, 2004. With Jean-Marc Talbot. We study the complexity of the model-checking problem for the tree logic introduced as the basis for the query language TQL [Cardelli, Ghelli 01: Query Language Based on the Ambient Logic]. We define two distinct fragments of this logic: TL containing only spatial connectives and TLe containing spatial connectives and quantification. We show that the combined complexity of TL is PSPACE-hard. We also study data complexity of model-checking and show that it is linear for TL, hard for all levels of the polynomial hierarchy for TLe and PSPACE-hard for the full logic. Finally we devise a polynomial space model-checking algorithm showing this way that the model-checking problem for the TQL logic is PSPACE-complete.
## Model-checking du fragment spatial de la logique des ambientsIn Manifestation des Jeunes Chercheurs STIC - MAJECSTIC'03, 2003. La logique des ambients est une logique modale introduite initialement pour la modélisation de propriétés des processus du calcul des ambients. Son fragment spatial modélise la structure des processus, c'est à dire des arbres non-ordonnés. Cette logique a déjà été étudiée par L. Cardelli et G. Ghelli sous la dénomination TQL et utilisée pour la définition d'un langage de requêtes pour documents semi-structurés. Nous nous intéressons dans cet article du modelchecking de cette logique et de sa complexité.
Dans une première partie nous définissons la logique ainsi que le modèle d'arbres sous-jacent. Il s'agit d'arbres non-ordonnés et d'arité non-bornée, étiquetés sur les arêtes par un ensemble infini de labels. La logique présentée possède un grand nombre d'opérateurs, dont la quantification existentielle sur les labels et sur les arbres, comparaison de labels, et un opérateur de plus petit point fixe. Nous illustrons par quelques exemples la possibilité d'utilisation de cette logique pour la recherche d'informations dans des documents semi-structurés.
Nous définissons ensuite la notion de modèle pour la logique et étudions ses propriétés de satisfiabilitee, ce qui nous permet de définir un algorithme de modelchecking. Nous montrons ensuite que la complexité du problème de model-checking est minorée par la classe de complexité PSPACE-difficile. Nous terminons en présentant quelques perspectives pour la définition de logiques d'arbres non-ordonnés de moindre complexité.
## Graphs for object oriented verification## A Modal-Logic Based Graph Abstraction. .In 4th International Conference on Graph Transformation. With Jörg Bauer, Arend Rensink and Marcos Kurbán. Infinite or very large state spaces often prohibit the successful verification of graph transformation systems. Abstract graph transformation is an approach that tackles this problem by abstracting graphs to abstract graphs of bounded size and by lifting application of productions to abstract graphs. In this work, we present a new framework of abstractions unifying and generalising existing takes on abstract graph transformation. The precision of the abstraction can be adjusted according to the properties to be verified facilitating abstraction refinement. We present a modal logic defined on graphs, which is preserved and reflected by our abstractions.
Finally, we demonstrate the usability of the framework by verifying a graph transformation model of a firewall.
## Graph Abstraction and Abstract Graph Transformations.Technical report, University of Twente, 2007. With Arend Rensink, Marcos E. Kurbán, Jörg Bauer Many important systems like concurrent heap-manipulating programs, communication networks, or distributed algorithms are hard to verify due to their inherent dynamics and unboundedness. Graphs are an intuitive representation of states of these systems, where transitions can be conveniently described by graph transformation rules.
We present a framework for the abstraction of graphs supporting abstract graph transformation. The abstraction method naturally generalises previous approaches to abstract graph transformation. The set of possible abstract graphs is finite. This has the pleasant consequence of generating a finite transition system for any start graph and any finite set of transformation rules. Moreover, abstraction preserves a simple logic for expressing properties on graph nodes. The precision of the abstraction can be adjusted according to properties expressed in this logic to be verified.
## Generation of Sierpinski Triangles: A Case Study for Graph Transformation ToolsIn Proceedings of the third International Workshop and Symposium on Applications of Graph Transformation with Industrial Relevance (AGTIVE 2007). To appear. With Gabriele Taentzer, Enrico Biermann, Denes Bisztray, Bernd Bohnet, Artur Boronat, Leif Geiger, Rubino Geiss, Akos Horvath, Ole Kniemeyer, Tom Mens, Benjamin Ness, Detlef Plump, Tamas Vajk. This paper presents the different solutions of the Sierpinski Triangles case study for the Agtive'2007 graph transformation tools contest, among which the solution using the Groove tool.
## Simulating Multigraph Transformations Using Simple GraphsIn Proceedings of the 6th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2007), 2007, Volume 6 of Electronic Communications of the EASST, With Frank Hermann, Harmen Kastenberg and Arend Rensink. Application of graph transformations for software verification and model transformation is an emergent field of research. In particular, graph transformation approaches provide a natural way of modelling object oriented systems and semantics of object-oriented languages.
There exist a number of tools for graph transformations that are often specialised in a particular kind of graphs and/or graph transformation approaches, depending on the desired application domain. The main drawback of this diversity is the lack of interoperability.
In this paper we show how (typed) multigraph production systems can be translated into (typed) simple-graph production systems. The presented construction enables the use of multigraphs with DPO transformation approach in tools that only support simple graphs with SPO transformation approach, e.g. the GROOVE tool.
## Process algebra## When Ambients Cannot be OpenedIn Theoretical Computer Science, (333):127--169. Elsevier, 2005. With Jean-Marc Talbot. We investigate expressiveness of a fragment of the ambient calculus, a formalism for describing distributed and mobile computations. More precisely, we study expressiveness of the pure and public ambient calculus from which the capability open has been removed, in terms of the reachability problem of the reduction relation. Surprisingly, we show that even for this very restricted fragment, the reachability problem is not decidable. At a second step, for a slightly weaker reduction relation, we prove that reachability can be decided by reducing this problem to markings reachability for Petri nets. Finally, we show that the name-convergence problem as well as the model-checking problem turn out to be undecidable for both the original and the weaker reduction relation.
## When Ambients Cannot be OpenedIn Sixth International Conference on Foundations of Software Science and Computation Structures - FOSSACS 2003. Lecture Notes in Computer Science (2620). Springer Verlag, 2003. With Jean-Marc Talbot. We investigate expressiveness of a fragment of the ambient calculus, a formalism for describing distributed and mobile computations. More precisely, we study expressiveness of the pure and public ambient calculus from which the capability open has been removed, in terms of the reachability problem of the reduction relation. Surprisingly, we show that even for this very restricted fragment, the reachability problem is not decidable. At a second step, for a slightly weaker reduction relation, we prove that reachability can be decided by reducing this problem to markings reachability for Petri nets. Finally, we show that the name-convergence problem as well as the model-checking problem turn out to be undecidable for both the original and the weaker reduction relation.
## Doctorate thesis## Expressiveness, satisfiability and model checking of a spatial logic for unordered trees |