Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userAutomated Verification, Synthesis and Correction of Concurrent Systems via MSO Logic
105
0
0.0
(
0
)
Added by
Mateus de Oliveira Oliveira
Publication date
2014
fields
Informatics Engineering
and research's language is
English
Authors
Mateus de Oliveira Oliveira
Ask ChatGPT about the research
No Arabic abstract
In this work we provide algorithmic solutions to five fundamental problems concerning the verification, synthesis and correction of concurrent systems that can be modeled by bounded p/t-nets. We express concurrency via partial orders and assume that behavioral specifications are given via monadic second order logic. A c-partial-order is a partial order whose Hasse diagram can be covered by c paths. For a finite set T of transitions, we let P(c,T,phi) denote the set of all T-labelled c-partial-orders satisfying phi. If N=(P,T) is a p/t-net we let P(N,c) denote the set of all c-partially-ordered runs of N. A (b, r)-bounded p/t-net is a b-bounded p/t-net in which each place appears repeated at most r times. We solve the following problems: 1. Verification: given an MSO formula phi and a bounded p/t-net N determine whether P(N,c)subseteq P(c,T,phi), whether P(c,T,phi)subseteq P(N,c), or whether P(N,c)cap P(c,T,phi)=emptyset. 2. Synthesis from MSO Specifications: given an MSO formula phi, synthesize a semantically minimal (b,r)-bounded p/t-net N satisfying P(c,T,phi)subseteq P(N, c). 3. Semantically Safest Subsystem: given an MSO formula phi defining a set of safe partial orders, and a b-bounded p/t-net N, possibly containing unsafe behaviors, synthesize the safest (b,r)-bounded p/t-net N whose behavior lies in between P(N,c)cap P(c,T,phi) and P(N,c). 4. Behavioral Repair: given two MSO formulas phi and psi, and a b-bounded p/t-net N, synthesize a semantically minimal (b,r)-bounded p/t net N whose behavior lies in between P(N,c) cap P(c,T,phi) and P(c,T,psi). 5. Synthesis from Contracts: given an MSO formula phi^yes specifying a set of good behaviors and an MSO formula phi^no specifying a set of bad behaviors, synthesize a semantically minimal (b,r)-bounded p/t-net N such that P(c,T,phi^yes) subseteq P(N,c) but P(c,T,phi^no ) cap P(N,c)=emptyset.
rate research
Read More
We present a collection of modular open source C++ libraries for the development of logic synthesis applications. These libraries can be used to develop applications for the design of classical and emerging technologies, as well as for the implementation of quantum compilers. All libraries are well documented and well tested. Furthermore, being header-only, the libraries can be readily used as core components in complex logic synthesis systems.
We consider the convex hull $P_{varphi}(G)$ of all satisfying assignments of a given MSO formula $varphi$ on a given graph $G$. We show that there exists an extended formulation of the polytope $P_{varphi}(G)$ that can be described by $f(|varphi|,tau)cdot n$ inequalities, where $n$ is the number of vertices in $G$, $tau$ is the treewidth of $G$ and $f$ is a computable function depending only on $varphi$ and $tau.$ In other words, we prove that the extension complexity of $P_{varphi}(G)$ is linear in the size of the graph $G$, with a constant depending on the treewidth of $G$ and the formula $varphi$. This provides a very general yet very simple meta-theorem about the extension complexity of polytopes related to a wide class of problems and graphs. As a corollary of our main result, we obtain an analogous result % for the weaker MSO$_1$ logic on the wider class of graphs of bounded cliquewidth. Furthermore, we study our main geometric tool which we term the glued product of polytopes. While the glued product of polytopes has been known since the 90s, we are the first to show that it preserves decomposability and boundedness of treewidth of the constraint matrix. This implies that our extension of $P_varphi(G)$ is decomposable and has a constraint matrix of bounded treewidth; so far only few classes of polytopes are known to be decomposable. These properties make our extension useful in the construction of algorithms.
The logic of equality with uninterpreted functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic to propositional formulas, we can apply Boolean methods such as Ordered Binary Decision Diagrams (BDDs) and Boolean satisfiability checkers to perform the verification. We can exploit characteristics of the formulas describing the verification conditions to greatly simplify the propositional formulas generated. In particular, we exploit the property that many equations appear only in positive form. We can therefore reduce the set of interpretations of the function symbols that must be considered to prove that a formula is universally valid to those that are ``maximally diverse. We present experimental results demonstrating the efficiency of this approach when verifying pipelined processors using the method proposed by Burch and Dill.
Most proof systems for concurrent programs assume the underlying memory model to be sequentially consistent (SC), an assumption which does not hold for modern multicore processors. These processors, for performance reasons, implement relaxed memory models. As a result of this relaxation a program, proved correct on the SC memory model, might execute incorrectly. To ensure its correctness under relaxation, fence instructions are inserted in the code. In this paper we show that the SC proof of correctness of an algorithm, carried out in the proof system of [Sou84], identifies per-thread instruction orderings sufficient for this SC proof. Further, to correctly execute this algorithm on an underlying relaxed memory model it is sufficient to respect only these orderings by inserting fence instructions.
The paper introduces a knowledge representation language that combines the event calculus with description logic in a logic programming framework. The purpose is to provide the user with an expressive language for modelling and analysing systems that evolve over time. The approach is exemplified with the logic programming language as implemented in the Fusemate system. The paper extends Fusemates rule language with a weakly DL-safe interface to the description logic $cal ALCIF$ and adapts the event calculus to this extended language. This way, time-stamped ABoxes can be manipulated as fluents in the event calculus. All that is done in the frame of Fusemates concept of stratification by time. The paper provides conditions for soundness and completeness where appropriate. Using an elaborated example it demonstrates the interplay of the event calculus, description logic and logic programming rules for computing possible models as plausible explanations of the current state of the modelled system.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
