Current graph query languages, including the standards SQL/PGQ and GQL, define their semantics in terms of sets of tuples. This is largely inadequate for data interoperability tasks such as data migration or data integration which require queries to output new property graphs. This demonstration showcases DTGraph, an open-source declarative rule-based framework for easily specifying and efficiently executing property graph transformations. We describe a novel comprehensive system that allows the declarative specification of property graph transformations, by extending openCypher queries with a new GENERATE clause for creating new property graphs. The system includes several modules: a parser, a compiler for translating the transformation logic into an efficient executable openCypher script, and an interface assisting users in developing their transformations. The demonstration showcases the ability of our framework to scale to large graph data, and its suitability for transforming real-world datasets.

Abstract We propose a superposition-based proof procedure to reason on equational first order formulas defined over graphs. First, we introduce the considered graphs that are directed labeled graphs with lists of roots standing for pins or interfaces for replacements. Then the syntax and semantics of the considered logic are defined. The formulas at hand are clause sets built on equations and disequations on graphs. Afterwards, a sound and complete proof procedure is provided, and redundancy criteria are introduced to dismiss useless clauses and improve the efficiency of the procedure. In a first step, a set of inferences rules is provided in the case of uninterpreted labels. In a second step, the proposed rules are lifted to take into account labels defined as terms interpreted in some arbitrary theory. Particular formulas of interest are Horn clauses, for which stronger redundancy criteria can be devised. Essential differences with the usual term superposition calculus are emphasized.

We introduce a class of rooted graphs which are expressive enough to encode various kinds of classical or quantum circuits. We then follow a set-theoretic approach to define rewrite systems over the considered graphs. Afterwards, we tackle the problem of equational reasoning with the graphs under study and we propose a new Superposition calculus to check the unsatisfiability of formulas consisting of equations or disequations over these graphs. We establish the soundness and refutational completeness of the calculus.

We consider the problem of verifying graph transformations described by an imperative programming language. This question is particularly relevant for transformation of knowledge bases. We will argue in this paper that previous proof approaches based on dedicated Description Logics were technically complex and often inappropriate for reasoning about preservation of structure of knowledge bases. For these reasons, we explore here an assertion formalism based on the Guarded Fragment of predicate logic, which provides a homogeneous framework. Based on a formal semantics of our transformation language, we show how to extract proof obligations from annotated programs and how to obtain decidable correctness problems.

Rewriting techniques constitute a foundational theory of computing science. They are being investigated for several structures, such as lambda-terms, strings, first-order terms or graphs, and have been successfully used in many areas such as programming languages, automated reasoning, program verification, security, etc. The growing interest in this research area is witnessed by the leading international events, such as ICGT (International Conference on Graph Transformation) and the recent FSCD conference (International Conference on Formal Structures for Computation and Deduction), which gathers all topics of the former international conferences RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications). During the last decade, a particular interest has been devoted to the study of the impact of shared structures in term and graph rewriting through the international workshops editions of TERMGRAPH and GCM (Graph Computation Models).

We tackle the problem of simultaneous transformations of networks represented as graphs. Roughly speaking, one may distinguish two kinds of simultaneous or parallel rewrite relations over complex structures such as graphs: (i) those which transform disjoint subgraphs in parallel and hence can be simulated by successive mere sequential and local transformations and (ii) those which transform overlapping subgraphs simultaneously. In the latter situations, parallel transformations cannot be simulated in general by means of successive local rewrite steps. We investigate this last problem in the framework of overlapping graph transformation systems. As parallel transformation of a graph does not produce a graph in general, we propose first some sufficient conditions that ensure the closure of graphs by parallel rewrite relations. Then we mainly introduce and discuss two parallel rewrite relations over graphs. One relation is functional and thus deterministic, the other one is not functional for which we propose sufficient conditions which ensure its confluence.

We define a new class of rewrite systems operating over term-graphs. Our aim is twofold. First we propose to extend classical first-order rewrite rules in order to process easily data-structures with pointers (e.g., circular lists, doubly linked lists etc). For that, our rules provide specific features such as pointer (edges) redirections, relabeling of existing nodes etc. Unfortunately, such features are very often source of non confluence. Our second aim is then to ensure confluence of the considered rewrite systems in the new class. We introduce the notion of term-graphs with priority and show that orthogonal rewrite systems are confluent in our setting

We address the problem of controlling information leakage in a concurrent declarative programming setting. Our aim is to define verification tools in order to distinguish between authorized, or declared, information flows such as password testing (e.g., ATM, login processes, etc.) and non-authorized ones. In this paper, we first propose a way to define security policies as confluent and terminating rewrite systems. Such policies define how the privacy levels of information evolve. Then, we provide a formal definition of secure processes with respect to a given security policy. We also define an actual verification algorithm of secure processes based on constraint solving.

We propose a new algorithm of secrecy analysis in a framework integrating declarative programming and concurrency. The analysis of a program ensures that information can only flow from less sensitive levels toward more sensitive ones. Our algorithm uses a terminating abstract operational semantics which reduces the problem of secrecy to constraint solving within finite lattices. It departs in that from the previous works essentially based on type systems. Furthermore, our proposal is general and tackles a very large class of programs, featuring dynamic process creation, general sequential composition, recursive process calls and high level synchronization.

We define a new generic operator, ∇, which can be used within any programming language which allows one to define discrete time intervals. Let Τ0, ..., Τn be the consecutive instants of an interval I, u a term and vΤi the value of u at instantΤi. We define the expression ∇(O,e,I) u as the first-order term (...((e O vΤ0) O vΤ1) ... O vΤn). We integrate this operator into timed rewrite systems, illustrate it through several examples and provide an efficient operational semantics which we have implemented.

We propose an efficient operational semantics for a new class of rewrite systems, namely timed rewrite systems. This class constitute a conservative extension of first-order conditional term rewrite systems together with time features such as clocks, signals, timed terms, timed atoms and timed rules. We define first timed rewrite systems and illustrate them through some examples. A naive approach to the operational semantics is very costly in space. We propose, for a large class of programs, an improved calculus with a linear space complexity. Finally, we show how our framework compares to related work.

Investigate the verification problem of infinite-state processes w.r.t. nonregular properties, i.e. nondefinable by finite-state /spl omega/-automata. We consider processes in the algebra PA (Process Algebra) which provides sequential and parallel (merge) composition, nondeterministic choice and recursion. The algebra PA integrates and strictly subsumes the algebras BPA (Basic Process Algebra, i.e. context-free processes) and BPP (Basic Parallel Processes). On the other hand, we consider properties definable in a new temporal logic called CLTL (Constrained Linear-Time Logic) which is an extension of the linear-time temporal logic LTL with two kinds of constraints on traces: constraints on the numbers of occurrences of states expressed using Presburger formulas (occurrence constraints), and constraints on the order of appearance of states expressed using finite-state automata (pattern constraints). Pattern constraints allow to capture all the /spl omega/-regular properties whereas occurrence constraints allow to define nonregular properties. Then, we present (un)decidability results concerning the verification problem for the different classes of processes mentioned above and different fragments of CLTL.

We investigate the verification problem of infinite-state process w.r.t. logic-based specifications that express properties which may be nonregular. We consider the process algebra PA which integrates and strictly subsumes the algebras BPA (basic process algebra) and BPP (basic parallel processes), by allowing both sequential and parallel compositions as well as nondeterministic choice and recursion. Many relevant properties of PA processes are nonregular, and thus can be expressed neither by classical temporal logics nor by finite state ω-automata. Properties of particular interest are those involving constraints on numbers of occurrences of events. In order to express such properties, which are nonregular in general, we use the temporal logic PCTL which combines the branching-time temporal logic CTL with Presburger arithmetics. Then we tackle the verification problem of guarded PA processes w.r.t. PCTL formulas. We mainly prove that, while this problem is undecidable for the full PCTL, it is actually decidable for the class of guarded PA processes (and thus for the class of guarded BPA's and guarded BPP's), and a large fragment of PCTL called PCTL+.

Narrowing is the operational principle of languages that integrate functional and logic programming. We propose a notion of a needed narrowing step that, for inductively sequential rewrite systems, extends the Huet and Le´vy notion of a needed reduction step. We define a strategy, based on this notion, that computes only needed narrowing steps. Our strategy is sound and complete for a large class of rewrite systems, is optimal w.r.t. the cost measure that counts the number of distinct steps of a derivation, computes only independent unifiers, and is efficiently implemented by pattern matching.

The verification problem for real-time properties involving duration constraints (predicates) is addressed. The duration of a state property, along an interval of a computation sequence of a real-time system, is the time the property is true. In particular, the global time spent in such an interval is the duration of the formula 'true'. The real-time logic TCTL is extended to a duration logic called SDTL in which duration constraints can be expressed. The problem of the verification of SDTL formulas with respect to a class of timed models of reactive systems is investigated. New model checking procedures are proposed for the most significant properties expressible in SDTL, including eventuality and invariance properties. Such results are provided for the two cases of discrete and dense time.>