17
17
Jun 28, 2018
06/18
by
Nikos Arechiga; James Kapinski; Jyotirmoy Deshmukh; Andre Platzer; Bruce Krogh
texts
eye 17
favorite 0
comment 0
The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid sys- tems; however, state-of-the-art theorem provers require ex- tensive manual intervention. Furthermore, there is often a gap between the type of assistance that a theorem prover requires to make progress on a proof task and the assis- tance that a system designer is able to provide. This paper presents an extension to KeYmaera, a deductive verification tool for differential...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1507.05133
13
13
Jun 28, 2018
06/18
by
Thomas Schwentick; Nils Vortmeier; Thomas Zeume
texts
eye 13
favorite 0
comment 0
A dynamic program, as introduced by Patnaik and Immerman (1994), maintains the result of a fixed query for an input database which is subject to tuple insertions and deletions. It can use an auxiliary database whose relations are updated via first-order formulas upon modifications of the input database. This paper studies static analysis problems for dynamic programs and investigates, more specifically, the decidability of the following three questions. Is the answer relation of a given dynamic...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1507.04537
11
11
Jun 28, 2018
06/18
by
Drewes Frank; Leroux Jérôme
texts
eye 11
favorite 0
comment 0
A Petri net is structurally cyclic if every configuration is reachable from itself in one or more steps. We show that structural cyclicity is decidable in deterministic polynomial time. For this, we adapt the Kosaraju's approach for the general reachability problem for Petri nets.
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1510.08331
6
6.0
Jun 30, 2018
06/18
by
Pablo F. Castro; Thomas S. E. Maibaum
texts
eye 6
favorite 0
comment 0
In this paper we investigate further the tableaux system for a deontic action logic we presented in previous work. This tableaux system uses atoms (of a given boolean algebra of action terms) as labels of formulae, this allows us to embrace parallel execution of actions and action complement, two action operators that may present difficulties in their treatment. One of the restrictions of this logic is that it uses vocabularies with a finite number of actions. In this article we prove that this...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1401.0969
8
8.0
Jun 30, 2018
06/18
by
Edward Hermann Haeusler
texts
eye 8
favorite 0
comment 0
In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic (M-imply) is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4, proved by Ladner, and the Goedel translation from S4 into Intuitionistic Logic, the PSPACE- completeness of M-imply is drawn. The sub-formula principle for a deductive system for a logic L states...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1401.8209
5
5.0
Jun 29, 2018
06/18
by
Benjamin Aminof; Sasha Rubin; Francesco Spegni; Florian Zuleger
texts
eye 5
favorite 0
comment 0
We consider the model checking problem of infinite state systems given in the form of parameterized discrete timed networks with multiple clocks. We show that this problem is decidable with respect to specifications given by B- or S-automata. Such specifications are very expressive (they strictly subsume omega-regular specifications), and easily express complex liveness and safety properties. Our results are obtained by modeling the passage of time using symmetric broadcast, and by solving the...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1609.04176
7
7.0
Jun 30, 2018
06/18
by
Andrea Asperti
texts
eye 7
favorite 0
comment 0
Automatic verification deals with the validation by means of computers of correctness certificates. The related tools, usually called proof assistants or interactive provers, provide an interactive environment for the creation of formal certificates whose correctness can be assessed in a purely automatic way. Such systems have applications both in mathematics, where certificates are proofs of theorems, and in computer science, where certificates testify the correctness of a given software with...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1701.03602
7
7.0
Jun 30, 2018
06/18
by
Simone Bova; Stefan Szeider
texts
eye 7
favorite 0
comment 0
The evaluation of a query over a probabilistic database boils down to computing the probability of a suitable Boolean function, the lineage of the query over the database. The method of query compilation approaches the task in two stages: first, the query lineage is implemented (compiled) in a circuit form where probability computation is tractable; and second, the desired probability is computed over the compiled circuit. A basic theoretical quest in query compilation is that of identifying...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1701.04626
5
5.0
Jun 30, 2018
06/18
by
Flavien Breuvart; Ugo Dal Lago; Agathe Herrou
texts
eye 5
favorite 0
comment 0
We study the expressive power of subrecursive probabilistic higher-order calculi. More specifically, we show that endowing a very expressive deterministic calculus like Godel's T with various forms of probabilistic choice operators may result in calculi which are not equivalent as for the class of distributions they give rise to, although they all guarantee almost-sure termination. Along the way, we introduce a probabilistic variation of the classic reducibility technique, and we prove that the...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1701.04786
6
6.0
Jun 30, 2018
06/18
by
Marco Voigt
texts
eye 6
favorite 0
comment 0
Recently, the separated fragment (SF) has been introduced and proved to be decidable. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. The known upper bound on the time required to decide SF's satisfiability problem is formulated in terms of quantifier alternations: Given an SF sentence $\exists \vec{z} \forall \vec{x}_1 \exists \vec{y}_1 \ldots \forall \vec{x}_n \exists \vec{y}_n . \psi$ in which $\psi$ is quantifier free,...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1704.02145
16
16
Jun 28, 2018
06/18
by
François Laroussinie; Nicolas Markey; Arnaud Sangnier
texts
eye 16
favorite 0
comment 0
Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that uniform incomplete observation (where all...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1509.07208
10
10.0
Jun 28, 2018
06/18
by
Parosh Abdulla; Giorgio Delzanno; Marco Montali
texts
eye 10
favorite 0
comment 0
We propose a formal model of concurrent systems in which the history of a computation is explicitly represented as a collection of events that provide a view of a sequence of configurations. In our model events generated by transitions become part of the system configurations leading to operational semantics with historical data. This model allows us to formalize what is usually done in symbolic verification algorithms. Indeed, search algorithms often use meta-information, e.g., names of fired...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1509.07203
6
6.0
Jun 28, 2018
06/18
by
Matteo Mio; Alex Simpson
texts
eye 6
favorite 0
comment 0
The paper explores properties of the {\L}ukasiewicz {\mu}-calculus, or {\L}{\mu} for short, an extension of {\L}ukasiewicz logic with scalar multiplication and least and greatest fixed-point operators (for monotone formulas). We observe that {\L}{\mu} terms, with $n$ variables, define monotone piecewise linear functions from $[0, 1]^n$ to $[0, 1]$. Two effective procedures for calculating the output of {\L}{\mu} terms on rational inputs are presented. We then consider the {\L}ukasiewicz modal...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1510.00797
8
8.0
Jun 29, 2018
06/18
by
Yongming Li
texts
eye 8
favorite 0
comment 0
Model checking of linear-time properties based on possibility measures was studied in previous work (Y. Li and L. Li, Model checking of linear-time properties based on possibility measure, IEEE Transactions on Fuzzy Systems, 21(5)(2013), 842-854). However, the linear-time properties considered in the previous work was classical and qualitative, possibility information of the systems was not considered at all. We shall study quantitative model checking of fuzzy linear-time properties based on...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1601.06504
7
7.0
Jun 29, 2018
06/18
by
Ken Akiba
texts
eye 7
favorite 0
comment 0
Classical (or Boolean) type theory is the type theory that allows the type inference $\sigma \to \bot) \to \bot => \sigma$ (the type counterpart of double-negation elimination), where $\sigma$ is any type and $\bot$ is absurdity type. This paper first presents a denotational semantics for a simplified version of Parigot's lambda-mu calculus, a premier example of classical type theory. In this semantics the domain of each type is divided into infinitely many ranks and contains not only the...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1606.06385
8
8.0
Jun 29, 2018
06/18
by
Pedro Cabalar; Jorge Fandinno
texts
eye 8
favorite 0
comment 0
In this paper, we study an extension of the stable model semantics for disjunctive logic programs where each true atom in a model is associated with an algebraic expression (in terms of rule labels) that represents its justifications. As in our previous work for non-disjunctive programs, these justifications are obtained in a purely semantic way, by algebraic operations (product, addition and application) on a lattice of causal values. Our new definition extends the concept of causal stable...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1608.00870
30
30
Jun 29, 2018
06/18
by
Jan A. Bergstra; Alban Ponse
texts
eye 30
favorite 0
comment 0
A datatype defining rewrite system (DDRS) is a ground-complete term rewriting system, intended to be used for the specification of datatypes. As a follow-up of an earlier paper we define two concise DDRSes for the ring of integers, each comprising only twelve rewrite rules, and prove their ground-completeness. Then we introduce DDRSes for a concise specification of natural number arithmetic and integer arithmetic in unary view, that is, arithmetic based on unary append (a form of tallying) or...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1608.06212
6
6.0
Jun 30, 2018
06/18
by
Sławomir Lasota
texts
eye 6
favorite 0
comment 0
We investigate the Constraint Satisfaction Problem (CSP) over templates with a group structure, and algorithms solving CSP that are equivariant, i.e. invariant under a natural group action induced by a template. Our main result is a method of proving the implication: if CSP over a coset template T is solvable by an equivariant algorithm then T is 2-Helly (or equivalently, has a majority polymorphism). Therefore bounded width, and definability in fixed-point logics, coincide with 2-Helly. Even...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1412.4020
21
21
Jun 26, 2018
06/18
by
Amnon Rosenmann
texts
eye 21
favorite 0
comment 0
We present a novel approach, which is based on multiple-valued logic (MVL), to the verification and analysis of digital hardware designs, which extends the common ternary or quaternary approaches for simulations. The simulations which are performed in the more informative MVL setting reveal details which are either invisible or harder to detect through binary or ternary simulations. In equivalence verification, detecting different behavior under MVL simulations may lead to the discovery of a...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1502.05748
15
15
Jun 27, 2018
06/18
by
Simon Außerlechner; Swen Jacobs; Ayrat Khalimov
texts
eye 15
favorite 0
comment 0
Guarded protocols were introduced in a seminal paper by Emerson and Kahlon (2000), and describe systems of processes whose transitions are enabled or disabled depending on the existence of other processes in certain local states. We study parameterized model checking and synthesis of guarded protocols, both aiming at formal correctness arguments for systems with any number of processes. Cutoff results reduce reasoning about systems with an arbitrary number of processes to systems of a...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1505.03273
12
12
Jun 27, 2018
06/18
by
Taolue Chen; Wan Fokkink; Rob van Glabbeek
texts
eye 12
favorite 0
comment 0
A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves omega-completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and omega-complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a finite,...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1505.04985
5
5.0
Jun 30, 2018
06/18
by
Linh Anh Nguyen; Joanna Golińska-Pilarek
texts
eye 5
favorite 0
comment 0
We give the first ExpTime (complexity-optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHOQ, which extends the basic description logic ALC with transitive roles, hierarchies of roles, nominals and quantified number restrictions. The complexity is measured using unary representation for numbers. Our procedure is based on global caching and integer linear feasibility checking.
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1405.7221
8
8.0
Jun 30, 2018
06/18
by
Kirstin Peters; Tsvetelina Yonova-Karbe; Uwe Nestmann
texts
eye 8
favorite 0
comment 0
We study whether, in the pi-calculus, the match prefix-a conditional operator testing two names for (syntactic) equality-is expressible via the other operators. Previously, Carbone and Maffeis proved that matching is not expressible this way under rather strong requirements (preservation and reflection of observables). Later on, Gorla developed a by now widely-tested set of criteria for encodings that allows much more freedom (e.g. instead of direct translations of observables it allows...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1408.1454
16
16
Jun 26, 2018
06/18
by
Ulrich Berger; Andrew Lawrence; Fredrik Nordvall Forsberg; Monika Seisenberger
texts
eye 16
favorite 0
comment 0
This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are correct by construction. To this end, we formalize a completeness proof for the DPLL proof system and extract a SAT solver from it. When applied to a propositional formula in conjunctive normal form the program produces either a satisfying assignment or a DPLL derivation showing its unsatisfiability....
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1502.02131
11
11
Jun 26, 2018
06/18
by
Florian Lonsing; Uwe Egly
texts
eye 11
favorite 0
comment 0
We consider the incremental computation of minimal unsatisfiable cores (MUCs) of QBFs. To this end, we equipped our incremental QBF solver DepQBF with a novel API to allow for incremental solving based on clause groups. A clause group is a set of clauses which is incrementally added to or removed from a previously solved QBF. Our implementation of the novel API is related to incremental SAT solving based on selector variables and assumptions. However, the API entirely hides selector variables...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1502.02484
37
37
Jun 26, 2018
06/18
by
Tomáš Brázdil; Krishnendu Chatterjee; Martin Chmelík; Andreas Fellner; Jan Křetínský
texts
eye 37
favorite 0
comment 0
While for deterministic systems, a counterexample to a property can simply be an error trace, counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1502.02834
16
16
Jun 26, 2018
06/18
by
Yan Zhang; Zhaohui Zhu; Jinjin Zhang
texts
eye 16
favorite 0
comment 0
In the framework of logic labelled transition system, a variant of weak ready simulation has been presented by L\"{u}ttgen and Vogler. It has been shown that such behavioural preorder is the largest precongruence w.r.t parallel and conjunction composition satisfying desired properties. This paper offers a ground-complete axiomatization for this precongruence over processes containing no recursion in the calculus $\text{CLL}_R$. Compared with usual inference system for process calculus, in...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1502.03636
21
21
Jun 26, 2018
06/18
by
Andrew Reynolds; Morgan Deters; Viktor Kuncak; Cesare Tinelli; Clark Barrett
texts
eye 21
favorite 0
comment 0
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided techniques for quantifier instantiation that we use to make finding such proofs practically feasible. A particularly important class of specifications are single-invocation properties, for which we present a dedicated algorithm. To support...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1502.04464
16
16
Jun 27, 2018
06/18
by
Jérôme Leroux; Sylvain Schmitz
texts
eye 16
favorite 0
comment 0
More than 30 years after their inception, the decidability proofs for reachability in vector addition systems (VAS) still retain much of their mystery. These proofs rely crucially on a decomposition of runs successively refined by Mayr, Kosaraju, and Lambert, which appears rather magical, and for which no complexity upper bound is known. We first offer a justification for this decomposition technique, by showing that it computes the ideal decomposition of the set of runs, using the natural...
Topics: Computing Research Repository, Logic in Computer Science
Source: http://arxiv.org/abs/1503.00745
12
12
Jun 27, 2018
06/18
by
Assalé Adjé; Pierre-Loïc Garoche; Victor Magron
texts
eye 12
favorite 0
comment 0
While abstract interpretation is not theoretically restricted to specific kinds of properties, it is, in practice, mainly developed to compute linear over-approximations of reachable sets, aka. the collecting semantics of the program. The verification of user-provided properties is not easily compatible with the usual forward fixpoint computation using numerical abstract domains. We propose here to rely on sums-of-squares programming to characterize a property-driven polynomial invariant. This...
Topics: Computing Research Repository, Logic in Computer Science
Source: http://arxiv.org/abs/1503.07025
12
12
Jun 27, 2018
06/18
by
Arnd Hartmanns; Holger Hermanns
texts
eye 12
favorite 0
comment 0
The applicability of model checking is hindered by the state space explosion problem in combination with limited amounts of main memory. To extend its reach, the large available capacities of secondary storage such as hard disks can be exploited. Due to the specific performance characteristics of secondary storage technologies, specialised algorithms are required. In this paper, we present a technique to use secondary storage for probabilistic model checking of Markov decision processes. It...
Topics: Computing Research Repository, Logic in Computer Science
Source: http://arxiv.org/abs/1504.02861
5
5.0
Jun 29, 2018
06/18
by
Bohua Zhan
texts
eye 5
favorite 0
comment 0
We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core algorithm is a best-first search through the space of propositions derivable from the initial assumptions, where new propositions are added by user-defined functions called proof steps. We implemented the prover in Isabelle/HOL, and applied it to several formalization projects in mathematics and computer science,...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1605.07577
4
4.0
Jun 29, 2018
06/18
by
Takayuki Kihara; Arno Pauly
texts
eye 4
favorite 0
comment 0
In computable analysis testing a real number for being zero is a fundamental example of a non-computable task. This causes problems for division: We cannot ensure that the number we want to divide by is not zero. In many cases, any real number would be an acceptable outcome if the divisor is zero - but even this cannot be done in a computable way. In this note we investigate the strength of the computational problem "Robust division": Given a pair of real numbers, the first not...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1606.04126
14
14
Jun 29, 2018
06/18
by
Simon Cruanes; Jasmin Christian Blanchette
texts
eye 14
favorite 0
comment 0
Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends for various proof assistants. In this short paper, we present some ideas to extend Nunchaku with partial support for dependent types and type classes, to make frontends for Coq and other systems based on dependent type theory more useful.
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1606.05945
3
3.0
Jun 29, 2018
06/18
by
Sam Sanders
texts
eye 3
favorite 0
comment 0
Kohlenbach's proof mining program deals with the extraction of effective information from typically ineffective proofs. Proof mining has its roots in Kreisel's pioneering work on the so-called unwinding of proofs. The proof mining of classical mathematics is rather restricted in scope due to the existence of sentences without computational content which are provable from the law of excluded middle and which involve only two quantifier alternations. By contrast, we show that the proof mining of...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1606.06386
3
3.0
Jun 29, 2018
06/18
by
Mario Alviano; Carmine Dodaro
texts
eye 3
favorite 0
comment 0
Unsatisfiable core analysis can boost the computation of optimum stable models for logic programs with weak constraints. However, current solvers employing unsatisfiable core analysis either run to completion, or provide no suboptimal stable models but the one resulting from the preliminary disjoint cores analysis. This drawback is circumvented here by introducing a progression based shrinking of the analyzed unsatisfiable cores. In fact, suboptimal stable models are possibly found while...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1608.00731
5
5.0
Jun 29, 2018
06/18
by
Christoph-Simon Senjak; Martin Hofmann
texts
eye 5
favorite 0
comment 0
The widely-used compression format "Deflate" is defined in RFC 1951 and is based on prefix-free codings and backreferences. There are unclear points about the way these codings are specified, and several sources for confusion in the standard. We tried to fix this problem by giving a rigorous mathematical specification, which we formalized in Coq. We produced a verified implementation in Coq which achieves competitive performance on inputs of several megabytes. In this paper we present...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1609.01220
3
3.0
Jun 29, 2018
06/18
by
Davide Bresolin; Emilio Muñoz-Velasco; Guido Sciavicco
texts
eye 3
favorite 0
comment 0
Modal logic is a paradigm for several useful and applicable formal systems in computer science. It generally retains the low complexity of classical propositional logic, but notable exceptions exist in the domains of description, temporal, and spatial logic, where the most expressive formalisms have a very high complexity or are even undecidable. In search of computationally well-behaved fragments, clausal forms and other sub-propositional restrictions of temporal and description logics have...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1609.04091
5
5.0
Jun 29, 2018
06/18
by
Lauri Hella; Antti Kuusisto; Arne Meier; Jonni Virtema
texts
eye 5
favorite 0
comment 0
Propositional and modal inclusion logic are formalisms that belong to the family of logics based on team semantics. This article investigates the model checking and validity problems of these logics. We identify complexity bounds for both problems, covering both lax and strict team semantics. By doing so, we come close to finalising the programme that ultimately aims to classify the complexities of the central reasoning problems for modal and propositional dependence, independence, and...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1609.06951
3
3.0
Jun 30, 2018
06/18
by
Shiguang Feng; Xishun Zhao
texts
eye 3
favorite 0
comment 0
This paper concerns Gradel's question asked in 1992: whether all problems which are in PTIME and closed under substructures are definable in second-order HORN logic SO-HORN. We introduce revisions of SO-HORN and DATALOG by adding first-order universal quantifiers over the second-order atoms in the bodies of HORN clauses and DATALOG rules. We show that both logics are as expressive as FO(LFP), the least fixed point logic. We also prove that FO(LFP) can not define all of the problems that are in...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1403.6611
3
3.0
Jun 30, 2018
06/18
by
Alejandro Díaz-Caro; Gilles Dowek
texts
eye 3
favorite 0
comment 0
We show how to provide a structure of probability space to the set of execution traces on a non-confluent abstract rewrite system, by defining a variant of a Lebesgue measure on the space of traces. Then, we show how to use this probability space to transform a non-deterministic calculus into a probabilistic one. We use as example Lambda+, a recently introduced calculus defined through type isomorphisms.
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1404.0081
3
3.0
Jun 30, 2018
06/18
by
Tomer Kotek; Mantas Simkus; Helmut Veith; Florian Zuleger
texts
eye 3
favorite 0
comment 0
We introduce a description logic ALCQIO_{b,Re} which adds reachability assertions to ALCQIO, a sub-logic of the two-variable fragment of first order logic with counting quantifiers. ALCQIO_{b,Re} is well-suited for applications in software verification and shape analysis. Shape analysis requires expressive logics which can express reachability and have good computational properties. We show that ALCQIO_{b,Re} can describe complex data structures with a high degree of sharing and allows...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1402.6804
5
5.0
Jun 30, 2018
06/18
by
Ugo Dal Lago; Claudia Faggian; Ichiro Hasuo; Akira Yoshimizu
texts
eye 5
favorite 0
comment 0
We graft synchronization onto Girard's Geometry of Interaction in its most concrete form, namely token machines. This is realized by introducing proof-nets for SMLL, an extension of multiplicative linear logic with a specific construct modeling synchronization points, and of a multi-token abstract machine model for it. Interestingly, the correctness criterion ensures the absence of deadlocks along reduction and in the underlying machine, this way linking logical and operational properties.
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1405.3427
4
4.0
Jun 30, 2018
06/18
by
Fedor Shmarov; Paolo Zuliani
texts
eye 4
favorite 0
comment 0
We develop an algorithm for computing bounded reachability probability for hybrid systems, i.e., the probability that the system reaches an unsafe region within a finite number of discrete transitions. In particular, we focus on hybrid systems with continuous dynamics given by solutions of nonlinear ordinary differential equations (with possibly nondeterministic initial conditions and parameters), and probabilistic behaviour given by initial parameters distributed as continuous (with possibly...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1406.1920
3
3.0
Jun 30, 2018
06/18
by
Truls Pedersen; Sjur Dyrkolbotn
texts
eye 3
favorite 0
comment 0
We consider multi-agent argumentation, where each agent's view of the arguments is encoded as an argumentation framework (AF). Then we study deliberative processes than can occur on this basis. We think of a deliberative process as taking the shape of a stepwise aggregation of a single joint AF, and we are interested in reasoning about the space of possible outcomes. The only restriction we place on deliberative processes is that they should satisfy faithfulness, a postulate amounting to...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1408.1647
3
3.0
Jun 30, 2018
06/18
by
Yuguo He
texts
eye 3
favorite 0
comment 0
We study a natural hierarchy in first-order logic, namely the quantifier structure hierarchy, which gives a systematic classification of first-order formulas based on structural quantifier resource. We define a variant of Ehrenfeucht-Fraisse games that characterizes quantifier classes and use it to prove that this hierarchy is strict over finite structures, using strategy compositions. Moreover, we prove that this hierarchy is strict even over ordered finite structures, which is interesting in...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1409.7488
3
3.0
Jun 30, 2018
06/18
by
Tom Hirschowitz
texts
eye 3
favorite 0
comment 0
In previous work with Pous, we defined a semantics for CCS which may both be viewed as an innocent form of presheaf semantics and as a concurrent form of game semantics. We define in this setting an analogue of fair testing equivalence, which we prove fully abstract w.r.t. standard fair testing equivalence. The proof relies on a new algebraic notion called playground, which represents the `rule of the game'. From any playground, we derive two languages equipped with labelled transition systems,...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1409.8056
10
10.0
Jun 27, 2018
06/18
by
Samuel Mimram
texts
eye 10
favorite 0
comment 0
We introduce a monoidal category whose morphisms are finite partial orders, with chosen minimal and maximal elements as source and target respectively. After recalling the notion of presentation of a monoidal category by the means of generators and relations, we construct a presentation of our category, which corresponds to a variant of the notion of bialgebra.
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1505.07161
3
3.0
Jun 30, 2018
06/18
by
Tobias Isenberg; Heike Wehrheim
texts
eye 3
favorite 0
comment 0
Proof-carrying hardware (PCH) is an approach to achieving safety of dynamically reconfigurable hardware, transferring the idea of proof-carrying code to the hardware domain. Current PCH approaches are, however, either limited to combinational and bounded unfoldings of sequential circuits, or only provide semi-automatic proof generation. We propose a new approach to PCH which employs IC3 as proof generator, making automatic PCH applicable to sequential circuits in their full generality. We...
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1410.4507
5
5.0
Jun 30, 2018
06/18
by
Colm Ó Dúnlaing
texts
eye 5
favorite 0
comment 0
It is fairly easy to show that every regular set is an almost-confluent congruential language (ACCL), and it is known that every regular set is a Church-Rosser congruential language (CRCL). Whether there exists an ACCL, which is not a CRCL, seems to remain an open question. In this note we present one such ACCL.
Topics: Logic in Computer Science, Computing Research Repository
Source: http://arxiv.org/abs/1411.5853
