We present a new approach for the design of a synthetic biological circuit whose behaviour is specified in terms of signal temporal logic (STL) formulae. We first show how to characterise with STL formulae the input/output behaviour of biological modules miming the classical logical gates (AND, NOT, OR). Hence, we provide the regions of the parameter space for which these specifications are satisfied. Given a STL specification of the target circuit to be designed and the networks of its constituent components, we propose a methodology to constrain the behaviour of each module, then identifying the subset of the parameter space in which those constraints are satisfied, providing also a measure of the robustness for the target circuit design. This approach, which leverages recent results on the quantitative semantics of Signal Temporal Logic, is illustrated by synthesising a biological implementation of an half-adder.
Modular logic programs provide a way of viewing logic programs as consisting of many independent, meaningful modules. This paper introduces first-order modular logic programs, which can capture the meaning of many answer set programs. We also introduce conservative extensions of such programs. This concept helps to identify strong relationships between modular programs as well as between traditional programs. We show how the notion of a conservative extension can be used to justify the common projection rewriting. This note is under consideration for publication in Theory and Practice of Logic…
Nowadays, numerous services based on large-scale distributed systems have been developed to boost the convenience of human life. On the other side, it becomes a significant challenge to ensure the correctness and properties of these systems due to the complex and nested architecture. Although concurrent separation logic (CSL) has partially tackled the problem by specifying systems and verifying the correctness of them, it faces modularity issues. In this paper, we propose an extended concurrent separation logic (ECSL) to address the modularity issues of CSL with the support of the temporal ext…
In this paper we show that states, transitions and behavior of concurrent systems can often be modeled as sheaves over a suitable topological space. In this context, geometric logic can be used to describe which local properties (i.e. properties of individual systems) are preserved, at a global level, when interconnecting the systems. The main area of application is to modular verification of complex systems. We illustrate the ideas by means of an example involving a family of interacting controllers for trains on a rail track.
This paper explores goal-directed proof search in first-order multi-modal logic. The key issue is to design a proof system that respects the modularity and locality of assumptions of many modal logics. By forcing ambiguities to be considered independently, modular disjunctions in particular can be used to construct efficiently executable specifications in reasoning tasks involving partial information that otherwise might require prohibitive search. To achieve this behavior requires prior proof-theoretic justifications of logic programming to be extended, strengthened, and combined with proof-t…
Technische Universität Dresden（德累斯顿工业大学）；Institute of Artificial Intelligence（人工智能研究所）
We introduce a framework that allows for the construction of sequent systems for expressive description logics extending ALC. Our framework not only covers a wide array of common description logics, but also allows for sequent systems to be obtained for extensions of description logics with special formulae that we call "role relational axioms." All sequent systems are sound, complete, and possess favorable properties such as height-preserving admissibility of common structural rules and height-preserving invertibility of rules.
Computer-Controlled Systems (CCS) are a subclass of hybrid systems where the periodic relation of control components to time is paramount. Since they additionally are at the heart of many safety-critical devices, it is of primary importance to correctly model such systems and to ensure they function correctly according to safety requirements. Differential dynamic logic $d\mathcal{L}$ is a powerful logic to model hybrid systems and to prove their correctness. We contribute a component-based modeling and reasoning framework to $d\mathcal{L}$ that separates models into components with timing guar…
Adding modular predicates yields a generalization of first-order logic FO over words. The expressive power of FO[<,MOD] with order comparison $x<y$ and predicates for $x \equiv i \mod n$ has been investigated by Barrington, Compton, Straubing and Therien. The study of FO[<,MOD]-fragments was initiated by Chaubard, Pin and Straubing. More recently, Dartois and Paperman showed that definability in the two-variable fragment FO2[<,MOD] is decidable. In this paper we continue this line of work. We give an effective algebraic characterization of the word languages in Sigma2[<,MOD]. The fragment Sigm…
CENTRIA - Centre for Artificial Intelligence（CENTRIA人工智能中心）；Universidade Nova de Lisboa（里斯本新大学）
Even though modularity has been studied extensively in conventional logic programming, there are few approaches on how to incorporate modularity into Answer Set Programming, a prominent rule-based declarative programming paradigm. A major approach is Oikarinnen and Janhunen's Gaifman-Shapiro-style architecture of program modules, which provides the composition of program modules. Their module theorem properly strengthens Lifschitz and Turner's splitting set theorem for normal logic programs. However, this approach is limited by module conditions that are imposed in order to ensure the compatib…
We investigate a recent proposal for modal hypersequent calculi. The interpretation of relational hypersequents incorporates an accessibility relation along the hypersequent. These systems give the same interpretation of hypersequents as Lellman's linear nested sequents, but were developed independently by Restall for S5 and extended to other normal modal logics by Parisi. The resulting systems obey Dosen's principle: the modal rules are the same across different modal logics. Different modal systems only differ in the presence or absence of external structural rules. With the exception of S5,…
Synthetic Biology is an interdisciplinary field that utilizes well-established engineering principles, ranging from electrical, control and computer systems, for analyzing the biological systems, such as biological circuits, enzymes, pathways and controllers. Traditionally, these biological systems, i.e., the genetic circuits are analyzed using paper-and-pencil proofs and computer-based simulations techniques. However, these methods cannot provide accurate results due to their inherent limitations such as human error-proneness, round-off errors and the unverified algorithms present in the core…
University of Kentucky（肯塔基大学）；Technische Universität Wien（维也纳工业大学）
A recent framework of relativized hyperequivalence of programs offers a unifying generalization of strong and uniform equivalence. It seems to be especially well suited for applications in program optimization and modular programming due to its flexibility that allows us to restrict, independently of each other, the head and body alphabets in context programs. We study relativized hyperequivalence for the three semantics of logic programs given by stable, supported and supported minimal models. For each semantics, we identify four types of contexts, depending on whether the head and body alpha…
Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further away from first-order logic, the logic of most automatic theorem provers. In this article, we develop a methodology to transform a subset of Coq goals into first-order statements that can be automatically discharged by automatic provers. The general idea is to write modular, pairwise independent transformations and combine them. Each of these eliminates a spec…
The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between objects in the heap. Reasoning about reachability is difficult for two main reasons. First, any heap modification may affect an unbounded number of reference chains, which complicates modular verification, in particular, framing. Second, general graph reachability is not supported by SMT solvers, which impedes automatic verification. In this paper, we present a modular specification and verification technique for reachability properties in separat…
We advocates here the use of (mathematical) logic for systems biology, as a unified framework well suited for both modeling the dynamic behaviour of biological systems, expressing properties of them, and verifying these properties. The potential candidate logics should have a traditional proof theoretic pedigree (including a sequent calculus presentation enjoying cut-elimination and focusing), and should come with (certified) proof tools. Beyond providing a reliable framework, this allows the adequate encodings of our biological systems. We present two candidate logics (two modal extensions of…
We study the complexity of reasoning tasks for logics in team semantics. Our main focus is on the data complexity of model checking but we also derive new results for logically defined counting and enumeration problems. Our approach is based on modular reductions of these problems into the corresponding problems of various classes of Boolean formulas. We illustrate our approach via several new tractability/intractability results.
Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are "abstract" because they are independent of any particular concrete resource model. Their assertion languages, called propositional abstract separation logics (PASLs), extend the logic of (Boolean) Bunched Implications (BBI) in various ways. In particular, these logics contain the connectives $*$ and $-\!*$, denoting the composition and extension of resources respectively. This added expressive power comes at a price since the res…
We report on intermediate results of our research on reasoning about liveness properties in addition to deep correctness properties for an imperative, concurrent programming language with a higher-order store. At present, we focus on one particular liveness property, namely termination. By guaranteeing termination we can strengthen statements of partial correctness to total correctness. This is achieved by the classic approach of turning termination into a safety property. In particular we extend the programming language under consideration with call permissions, which have been shown to enabl…
We propose an actor-critic, model-free, and online Reinforcement Learning (RL) framework for continuous-state continuous-action Markov Decision Processes (MDPs) when the reward is highly sparse but encompasses a high-level temporal structure. We represent this temporal structure by a finite-state machine and construct an on-the-fly synchronised product with the MDP and the finite machine. The temporal structure acts as a guide for the RL agent within the product, where a modular Deep Deterministic Policy Gradient (DDPG) architecture is proposed to generate a low-level control policy. We evalua…
We investigate the decidability of the definability problem for fragments of first order logic over finite words enriched with modular predicates. Our approach aims toward the most generic statements that we could achieve, which successfully covers the quantifier alternation hierarchy of first order logic and some of its fragments. We obtain that deciding this problem for each level of the alternation hierarchy of both first order logic and its two-variable fragment when equipped with all regular numerical predicates is not harder than deciding it for the corresponding level equipped with only…
Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance
TU Delft（代尔夫特理工大学）；Saarland University（萨尔大学）；National Institute of Informatics（信息学研究所）；Rice University（莱斯大学）；NII & SOKENDAI（信息学研究所与综合研究大学院大学）；Kyoto University & NII（京都大学与信息学研究所）；Université Sorbonne Paris Nord（巴黎北索邦大学）；Mitsubishi Electric Corporation（三菱电机株式会社）
本文针对 ISO 34502 标准中的关键驾驶场景，提出基于信号时序逻辑和 RSS 安全距离的模块化形式化方法，并通过实验验证其有效性与参数稳定性。
Hoare-style program logics are a popular and effective technique for software verification. Relational program logics are an instance of this approach that enables reasoning about relationships between the execution of two or more programs. Existing relational program logics have focused on verifying that all runs of a collection of programs do not violate a specified relational behavior. Several important relational properties, including refinement and noninterference, do not fit into this category, as they also mandate the existence of specific desirable executions. This paper presents RHLE,…
We propose a novel approach for the formal verification of biological systems based on the use of a modal linear logic. We show how such a logic can be used, with worlds as instants of time, as an unified framework to encode both biological systems and temporal properties of their dynamic behaviour. To illustrate our methodology, we consider a model of the P53/Mdm2 DNA-damage repair mechanism. We prove several properties that are important for such a model to satisfy and serve to illustrate the promise of our approach. We formalize the proofs of these properties in the Coq Proof Assistant, wit…
The main difficulty when modelling gene networks is the identification of the parameters that govern their dynamics. It is particularly difficult for models in which time is continuous: parameters have real values which cannot be enumerated. The widespread idea is to infer new constraints that reduce the range of possible values. Here we present a new work based on a particular class of Hybrid automata (inspired by Thomas discrete models) where discrete parameters are replaced by signed celerities. We propose a new approach involving Hoare logic and weakest precondition calculus (a la Dijkstra…
The University of Iowa（爱荷华大学）；University of Oxford（牛津大学）；University of Science and Technology of China（中国科学技术大学）
This paper investigates the motion planning of autonomous dynamical systems modeled by Markov decision processes (MDP) with unknown transition probabilities over continuous state and action spaces. Linear temporal logic (LTL) is used to specify high-level tasks over infinite horizon, which can be converted into a limit deterministic generalized Büchi automaton (LDGBA) with several accepting sets. The novelty is to design an embedded product MDP (EP-MDP) between the LDGBA and the MDP by incorporating a synchronous tracking-frontier function to record unvisited accepting sets of the automaton, a…
Effect algebras are one of the generalizations of Boolean algebras proposed in the quest for a quantum logic. Frobenius algebras are a tool of categorical quantum mechanics, used to present various families of observables in abstract, often nonstandard frameworks. Both effect algebras and Frobenius algebras capture their respective fragments of quantum mechanics by elegant and succinct axioms; and both come with their conceptual mysteries. A particularly elegant and mysterious constraint, imposed on Frobenius algebras to characterize a class of tripartite entangled states, is the antispecial l…
The past few years have seen a surge of interest in the field of probabilistic logic learning and statistical relational learning. In this endeavor, many probabilistic logics have been developed. ProbLog is a recent probabilistic extension of Prolog motivated by the mining of large biological networks. In ProbLog, facts can be labeled with probabilities. These facts are treated as mutually independent random variables that indicate whether these facts belong to a randomly sampled program. Different kinds of queries can be posed to ProbLog programs. We introduce algorithms that allow the effici…
University of Corunna（拉科鲁尼亚大学）；University of Potsdam（波茨坦大学）；University of Nebraska Omaha（内布拉斯加大学奥马哈分校）
In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate…
The paper introduces a new modular action language, ALM, and illustrates the methodology of its use. It is based on the approach of Gelfond and Lifschitz (1993; 1998) in which a high-level action language is used as a front end for a logic programming system description. The resulting logic programming representation is used to perform various computational tasks. The methodology based on existing action languages works well for small and even medium size systems, but is not meant to deal with larger systems that require structuring of knowledge. ALM is meant to remedy this problem. Structurin…
Taking an algebraic perspective on the basic structures of Rough Concept Analysis as the starting point, in this paper we introduce some varieties of lattices expanded with normal modal operators which can be regarded as the natural rough algebra counterparts of certain subclasses of rough formal contexts, and introduce proper display calculi for the logics associated with these varieties which are sound, complete, conservative and with uniform cut elimination and subformula property. These calculi modularly extend the multi-type calculi for rough algebras to a `nondistributive' (i.e. general …
