Reactive systems, (semi-)saturated semantics and coalgebras on presheaves

The semantics of process calculi has traditionally been specified by labelled transition systems (ltss), but, with the development of name calculi, it turned out that reaction rules (i.e., unlabelled transition rules) are often more natural. This leads to the question of how behavioral equivalences (bisimilarity, trace equivalence, etc.) defined for lts can be transferred to unlabelled transition systems. Recently, in order to answer this question, several proposals have been made with the aim of automatically deriving an lts from reaction rules in such a way that the resulting equivalences are congruences. Furthermore, these equivalences should agree with the standard semantics, whenever one exists.In this paper, we propose saturated semantics, based on a weaker notion of observation and orthogonal to all the previous proposals, and we demonstrate the appropriateness of our semantics by means of two examples: logic programming and open Petri nets. We also show that saturated semantics can be efficiently characterized through the so called semi-saturated games. Finally, we provide coalgebraic models relying on presheaves.     

A semantic framework for open processes

We propose a general methodology for analysing the behaviour of open systems modelled as coordinators, i.e., open terms of suitable process calculi. A coordinator is understood as a process with holes or placeholders where other coordinators and components (i.e., closed terms) can be plugged in, thus influencing its behaviour. The operational semantics of coordinators is given by means of a symbolic transition system, where states are coordinators and transitions are labeled by spatial/modal formulae expressing the potential interaction that plugged components may enable. Behavioural equivalences for coordinators, like strong and weak bisimilarities, can be straightforwardly defined over such a transition system. Different from other approaches based on universal closures, i.e., where two coordinators are considered equivalent when all their closed instances are equivalent, our semantics preserves the openness of the system during its evolution, thus allowing dynamic instantiation to be accounted for in the semantics. To further support the adequacy of the construction, we show that our symbolic equivalences provide correct approximations of their universally closed counterparts, coinciding with them over closed components. For process calculi in suitable formats, we show how tractable symbolic semantics can be defined constructively using unification.     

A sound and complete theory of graph transformations for service programming with sessions and pipelines

Graph transformation techniques, the Double-Pushout (DPO) approach in particular, have been successfully applied in the modeling of concurrent systems. In this area, a research thread has addressed the definition of concurrent semantics for process calculi. In this paper, we propose a theory of graph transformations for service programming with sophisticated features such as sessions and pipelines. Through graph representation of CaSPiS, a recently proposed process calculus, we show how graph transformations can cope with advanced features of service-oriented computing, such as several logical notions of scoping together with the interplay between linking and containment. We first exploit a graph algebra and set up a graph model that supports graph transformations in the DPO approach. Then, we show how to represent CaSPiS processes as hierarchical graphs in the graph model and their behaviors as graph transformation rules. Finally, we provide the soundness and completeness results of these rules with respect to the reduction semantics of CaSPiS.     

A Higher-Order Calculus for Graph Transformation

This paper presents a formalism for defining higher-order systems based on the notion of graph transformation (by rewriting or interaction). The syntax is inspired by the Combinatory Reduction Systems of Klop. The rewrite rules can be used to define first-order systems, such as graph or term-graph rewriting systems, Lafont's interaction nets, the interaction systems of Asperti and Laneve, the non-deterministic nets of Alexiev, or a process calculus. They can also be used to specify higher-order systems such as hierarchical graphs and proof nets of Linear Logic, or to specify the operational semantics of graph-based languages.     

From Chemical Rules to Term Rewriting

In this paper, rule-based programming is explored in the field of automated generation of chemical reaction mechanisms. We explore a class of graphs and a graph rewriting relation where vertices are preserved and only edges are changed. We show how to represent cyclic labeled graphs by decorated labeled trees or forests, then how to transform trees into terms. A graph rewriting relation is defined, then simulated by a tree rewriting relation, which can be in turn simulated by a rewriting relation on equivalence classes of terms. As a consequence, this kind of graph rewriting can be implemented using term rewriting. This study is motivated by the design of the GasEl system for the generation of kinetics reactions mechanisms. In GasEl, chemical reactions correspond to graph rewrite rules and are implemented by conditional rewriting rules in ELAN. The control of their application is done through the ELAN strategy language.     

Proximity-based federation of smart objects

Our real world environments today are filled with lots of embedded intelligent devices with communication capabilities like smart phone, embedded computers, sensor devices, etc., which we refer to as Smart Objects (SOs). Most ubiquitous computing applications are limited to the scope of two stereotyped scenarios, i.e., the location-transparent service continuation, and the context-aware service provision. Some researchers think that the potential of the ubiquitous and/or pervasive computing is limited because of the lack of its formal models. In our previous work, we introduced a new framework organized in a hierarchy of formal models. This framework allows the SOs to dynamically and autonomously reconstruct their federation configurations depending on their location and context change. This federation reconstruction is done without using any centralized control. A federation is modeled by a catalytic reaction which is inspired by a chemical reaction, and each application with a complex scenario of SO federations is modeled by a catalytic reaction network. We use graph rewriting rules to implement the federation mechanism, where the nodes and the edges of a graph respectively represent the SOs and their connections. This federation mechanism itself is inspired by the biological RNA (RiboNucleic Acid) replication mechanism. Here, we revise our framework and propose a new simplified set of graph rewriting rules for federating SOs as a catalytic reaction. This new set of rules is less complex and easier to understand. We also introduce an extra set of rules to deal with the exception handling that may occur during the federation process. Our main goal is to formally prove the validity of our rewriting rules for implementing any catalytic reaction. This guarantees both the generality and the correctness of out framework for implementing any complex federation scenarios that can be described as catalytic reaction networks.     

含假结RNA二级结构类的图语法

用最小自由能法预测RNA二级结构是NP困难问题,其根本原因是假结的存在。近几年的预测算法都针具有一定结构特征的假结寻找多项式时间算法进行预测。论文针对RNA二级结构图提出一种图语法,该语法由初始结构图集和重写规则集构成,用重写规则在初始结构图上的不断重写得到的结构图都是该语法的语言。分析了5个主流RNA二级结构预测算法的目标集,给出它们的图语法,使得目标集的结构特征一目了然,目标集间的真包含关系也通过图语法直观地体现出来。     

Graph rewriting systems for the entity-relationship approach

Sequential graph rewriting systems are proposed as a meta-level formalism providing the concise and sound definition of different ER diagram languages. These rewriting systems can be used to define ER-based approaches for various DB modelling subtasks like schema design, evolution and integration. In addition, they are a natural choice for syntax directed ER CASE workbenches. In particular, by using specialized ER graph rewriting systems as meta input for CASE tools, the resulting tool behavior can be guided and controlled. Moreover, grammar driven modelling tools can be easily adapted for the needs of a particular enterprise or software factory without superimposing a particular ER dialect on the end users. Additional benefits result from the use of ER graph rewriting systems as a comparison framework for the continuously enlarging set of ER dialects.

The presentation includes material on the ER graph rewriting formalism, i.e., the actual tool, as well as an introduction to some formal graph rewriting prerequisites. An exemplary application, in particular ER graph generation, is used to clarify the underlying formal concepts.     

Termination of High-Level Replacement Units with Application to Model Transformation

Visual rewriting techniques, in particular graph transformations, are increasingly used to model transformations of systems specified through diagrammatic sentences. Several rewriting models have been proposed, differing in the expressivity of the types of rules and in the complexity of the rewriting mechanism; yet basic results concerning the formal properties of these models are still missing for many of them. In this paper, we propose a contribution towards solving the termination problem for rewriting systems with external control mechanisms. In particular, we obtain results of more general validity by extending the concept of transformation unit to high-level replacement systems, a generalization of graph transformation systems. For high-level replacement units, we state and prove several abstract properties based on termination criteria. Then, we instantiate the high-level replacement systems by attributed graph transformation systems and present concrete termination criteria. These are used to show the termination of some replacement units needed to express model transformations as a consequence of software refactoring.     

Building Interpreters with Rewriting Strategies

Programming language semantics based on pure rewrite rules suffers from the gap between the rewriting strategy implemented in rewriting engines and the intended evaluation strategy. This paper shows how programmable rewriting strategies can be used to implement interpreters for programming languages based on rewrite rules. The advantage of this approach is that reduction rules are first class entities that can be reused in different strategies, even in other kinds of program transformations such as optimizers. The approach is illustrated with several interpreters for the lambda calculus based on implicit and explicit (parallel) substitution, different strategies including normalization, eager evaluation, lazy evaluation, and lazy evaluation with updates. An extension with pattern matching and choice shows that such interpreters can easily be extended.     

图卷积网络的抗混淆安卓恶意软件检测

自安卓发布以来,由于其开源、硬件丰富和应用市场多样等优势,安卓系统已经成为全球使用最广泛的手机操作系统。同时,安卓设备和安卓应用的爆炸式增长也使其成为96%移动恶意软件的攻击目标。现存的安卓恶意软件检测方法中,忽视程序语义而直接提取简单程序特征的方法检测速度快但精确度不理想,将程序语义转换为图模型并采用图分析的方法精确度高但开销大且扩展性低。为了解决上述挑战,本文将应用的程序语义提取为函数调用图,保留语义信息的同时采用抽象API技术将调用图转换为抽象图以减少运行开销并增强鲁棒性。基于得到的抽象图,以Triplet Loss损失训练构建基于图卷积神经网络的抗混淆安卓恶意软件分类器SriDroid。对20246个安卓应用进行实验分析之后,发现SriDroid可以达到99.17%的恶意软件检测精确度,并具有良好的鲁棒性。     

Conditional Term Graph Rewriting with Indirect Sharing

For reasons of efficiency, term rewriting is usually implemented by term graph rewriting. In term rewriting, expressions are represented as terms, whereas in term graph rewriting these are represented as directed graphs. Unlike terms, graphs allow a sharing of common subexpressions. In previous work, we have shown that conditional term graph rewriting is a sound and complete implementation for a certain class of CTRSs with strict equality, provided that a minimal structure sharing scheme is used. In this paper, we will show that this is also true for two different extensions of normal CTRSs. In contrast to the previous work, however, a non-minimal structure sharing scheme can be used. That is, the amount of sharing is increased.     

Lifting Infinite Normal Form Definitions From Term Rewriting to Term Graph Rewriting

nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.     

一种系统依赖图的面向对象扩充方案

提出一种对传统的系统依赖图进行面向对象扩充的方案.把传统的系统依赖图和类依赖子图、类层次子图相结合,从而构成了适合描述面向对象程序的面向对象系统依赖图.详细说明了对系统依赖图进行面向对象语法、语义扩充的过程,同时给出了构造面向对象系统依赖图的一般算法以及应用分析.     

A logical framework for querying and repairing inconsistent databases

In this paper, we address the problem of managing inconsistent databases, i.e., databases violating integrity constraints. We propose a general logic framework for computing repairs and consistent answers over inconsistent databases. A repair for a possibly inconsistent database is a minimal set of insert and delete operations which makes the database consistent, whereas a consistent answer is a set of tuples derived from the database, satisfying all integrity constraints. In our framework, different types of rules defining general integrity constraints, repair constraints (i.e., rules defining conditions on the insertion or deletion of atoms), and prioritized constraints (i.e., rules defining priorities among updates and repairs) are considered. We propose a technique based on the rewriting of constraints into (prioritized) extended disjunctive rules with two different forms of negation (negation as failure and classical negation). The disjunctive program can be used for two different purposes: to compute "repairs" for the database and produce consistent answers, i.e., a maximal set of atoms which do not violate the constraints. We show that our technique is sound, complete (each preferred stable model defines a repair and each repair is derived from a preferred stable model), and more general than techniques previously proposed.     

Domain-specific discrete event modelling and simulation using graph transformation

Graph transformation is being increasingly used to express the semantics of domain-specific visual languages since its graphical nature makes rules intuitive. However, many application domains require an explicit handling of time to accurately represent the behaviour of a real system and to obtain useful simulation metrics to measure throughputs, utilization times and average delays. Inspired by the vast knowledge and experience accumulated by the discrete event simulation community, we propose a novel way of adding explicit time to graph transformation rules. In particular, we take the event scheduling discrete simulation world view and provide rules with the ability to schedule the occurrence of other rules in the future. Hence, our work combines standard, efficient techniques for discrete event simulation (based on the handling of a future event set) and the intuitive, visual nature of graph transformation. Moreover, we show how our formalism can be used to give semantics to other timed approaches and provide an implementation on top of the rewriting logic system Maude.     

A fully abstract semantics for value-passing CCS for trees

We propose a fully abstract semantics for valuepassing CCS for trees (VCCTS) with the feature that processes are located at the vertices of a graph whose edges describe possible interaction capabilities. The operational semantics is given both in terms of a reduction semantics and in terms of a labelled transition semantics. We develop a theory of behavioral equivalences by introducing both weak barbed congruence and weak bisimilarity. In particular, we show that, on image-finite processes, weak barbed congruence coincides with weak bisimilarity. To illustrate potential applications and the powerful expressiveness of VCCTS, we formally compare VCCTS with some well-known models, e.g., dynamic pushdown networks, top-down tree automata and value-passing CCS.     

Translational relation embeddings for multi-hop knowledge base question answering

Multi-hop Knowledge Base Question Answering (KBQA) aims to predict answers that require multi-hop reasoning from the topic entity in the question over the Knowledge Base (KB). Relation extraction is a core step in KBQA, which extracts the relation path from the topic entity to the answer entity. Compared with single-hop questions, multi-hop ones have more complex syntactic structures to understand, and multi-hop relation paths lead to a larger search space, which makes it much more challenging to extract the correct relation paths. To tackle the above challenges, most existing relation extraction approaches focus on the semantic similarity between questions and relation paths. However, those approaches only consider the word semantics of the relation names but ignore the graph semantics inside the knowledge base. As a result, their generalization ability relying on the naming rules of the relations, making it more difficult to generalize over large knowledge bases.To address the current limitations and take advantage of the graph semantics of relations, we propose a novel translational embedding-based relation extractor that utilizes pretrained embeddings from TransE. In particular, we treat the multi-hop relation path as a translation from the first relation to the last one in the semantic space of TransE. Then we map the question into this space under the supervision of the path embeddings. To take full advantage of the pretrained graph semantics in TransE, we propose a KBQA framework that leverages pretrained relation semantics in relation extraction and pretrained entity semantics in answer selection. Our approach achieves state-of-the-art performance on two benchmark datasets, WebQuestionSP and MetaQA, demonstrating its effectiveness on the multi-hop KBQA task.     

Absolute versus Relative Time in Process Algebras

Timed process algebras are useful tools for the specification and verification of real-time systems. We study the relationships between two of these algebras, I (closed interval process Algebra) and TCCS (temporal CCS), which deal with temporal aspects of concurrent systems by following very different interpretations: durational actions versus durationless actions, absolute time versus relative time, timed functional behavior versus time and functional behavior, local clocks versus global clocks. We show that these different choices are not irreconcilable by presenting simple mappings from I to TCCS which preserve the behavioral equivalences over the two timed calculi. These results hold whenever basic actions are interpreted as either eager or lazy, whenever the starting time of action execution is observed rather than their completion time. A study on the size of the labelled transition systems describing the transitional semantics of cIpa processes and those describing the transitional semantics of their translated versions is also presented.