Search

Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraisse games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index k is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree-depth for the Ehrenfeucht-Fraisse comonad, tree-width for the pebbling comonad, and synchronization-tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science which hitherto have been almost disjoint: categorical semantics, and finite and algorithmic model theory., Comment: To appear in Proceedings of Computer Science Logic 2018

We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs, where in contrast to earlier work, our approach is not restricted to tail-recursion. Our technique constructs symbolic representations of program executions using a framework for iterative, under-approximating program simplification. The core of this simplification is a method for (under-approximating) program acceleration based on recurrence solving and a variation of ranking functions. Afterwards, we deduce asymptotic lower bounds from the resulting simplified programs using a special-purpose calculus and an SMT encoding. We implemented our technique in our tool LoAT and show that it infers non-trivial lower bounds for a large class of examples.

Two awards were made in 2021 to honour outstanding papers from the IEEE Symposium On Logic In Computer Science 2001 held in Boston, MA, USA.

One might poetically muse that computers have the essence both of logic and machines. Through the case of the history of Separation Logic, we explore how this assertion is more than idle poetry. Separation Logic works because it merges the software engineer’s conceptual model of a program’s manipulation of computer memory with the logical model that interprets what sentences in the logic are true, and because it has a proof theory which aids in the crucial problem of scaling the reasoning task. Scalability is a central problem, and some would even say the central problem, in appli- cations of logic in computer science. Separation Logic is an interesting case because of its widespread success in verification tools. For these two senses of model—the engineering/conceptual and the logical—to merge in a genuine sense, each must maintain their norms of use from their home disciplines. When this occurs, both the logic and engineering benefit greatly. Seeking this intersection of two different senses of model provides a strategy for how computer scientists and logicians may be successful. Furthermore, the history of Separation Logic for analysing programs provides a novel case for philosophers of science of how software engineers and computer scientists develop models and the components of such models. We provide three contributions: an exploration of the extent of models merging that is necessary for success in computer science; an introduction to the technical details of Separation Logic, which can be used for reasoning about other exhaustible resources; and an introduction to (a subset of) the problems, process, and results of computer scientists for those outside the field.

We prove that \(\omega \)-languages of (non-deterministic) Petri nets and \(\omega \)-languages of (non-deterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of \(\omega \)-languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of \(\omega \)-languages of (non-deterministic) Turing machines. We also show that it is highly undecidable to determine the topological complexity of a Petri net \(\omega \)-language. Moreover, we infer from the proofs of the above results that the equivalence and the inclusion problems for \(\omega \)-languages of Petri nets are \(\varPi _2^1\)-complete, hence also highly undecidable.

The textbook method for converting a first-order logic formula to prenex normal form potentially leads to an exponential growth of the formula size, if the formula is allowed to use all of the classical logical connectives ∧, ∨, →, ↔, ¬. This note presents a short proof which shows that the conversion is possible with polynomial growth of the formula size.

International audience; We consider existential problems over the reals. Extended quanti-fier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination for the quadratic case via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers , which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.

The program of the 30th Symposium on Logic in Computer Science held in 2015 in Kyoto included two contributions on the computational complexity of the reachability problem for vector addition systems: Blondin, Finkel, Göller, Haase, and McKenzie [2015] attacked the problem by providing the first tight complexity bounds in the case of dimension 2 systems with states, while Leroux and Schmitz [2015] proved the first complexity upper bound in the general case. The purpose of this column is to present the main ideas behind these two results, and more generally survey the current state of affairs.

We study a natural variant of the implicational fragment of propositional logic. Its formulas are pairs of conjunctions of positive literals, related together by an implicational-like connective; the semantics of this sort of implication is defined in terms of a threshold on a conditional probability of the consequent, given the antecedent: we are dealing with what the data analysis community calls confidence of partial implications or association rules. Existing studies of redundancy among these partial implications have characterized so far only entailment from one premise and entailment from two premises, both in the stand-alone case and in the case of presence of additional classical implications (this is what we call "relative entailment"). By exploiting a previously noted alternative view of the entailment in terms of linear programming duality, we characterize exactly the cases of entailment from arbitrary numbers of premises, again both in the stand-alone case and in the case of presence of additional classical implications. As a result, we obtain decision algorithms of better complexity; additionally, for each potential case of entailment, we identify a critical confidence threshold and show that it is, actually, intrinsic to each set of premises and antecedent of the conclusion.

We present the first approach to prove non-termination of integer programs that is based on loop acceleration. If our technique cannot show non-termination of a loop, it tries to accelerate it instead in order to find paths to other non-terminating loops automatically. The prerequisites for our novel loop acceleration technique generalize a simple yet effective non-termination criterion. Thus, we can use the same program transformations to facilitate both non-termination proving and loop acceleration. In particular, we present a novel invariant inference technique that is tailored to our approach. An extensive evaluation of our fully automated tool LoAT shows that it is competitive with the state of the art.

Women in Logic 2018, WiL2018, took place on July 8th 2018 in Oxford, as a workshop of the 33rd annual ACM/IEEE Symposium on Logic in Computer Science (LICS), part of the Federated Logic Conference 2018 (FLoC). It built on the success of the first such event, held in in Reykjavik, Iceland, in 2017, again in association with LICS.

Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraisse games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index k is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree-depth for the Ehrenfeucht-Fraisse comonad, tree-width for the pebbling comonad, and synchronization-tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science which hitherto have been almost disjoint: categorical semantics, and finite and algorithmic model theory.

We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counter-example guided inductive synthesis principle (CEGIS) and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs.

We present two novel algorithms for learning formulas in Linear Temporal Logic (LTL) from examples. The first learning algorithm reduces the learning task to a series of satisfiability problems in propositional Boolean logic and produces a smallest LTL formula (in terms of the number of subformulas) that is consistent with the given data. Our second learning algorithm, on the other hand, combines the SAT-based learning algorithm with classical algorithms for learning decision trees. The result is a learning algorithm that scales to real-world scenarios with hundreds of examples, but can no longer guarantee to produce minimal consistent LTL formulas. We compare both learning algorithms and demonstrate their performance on a wide range of synthetic benchmarks. Additionally, we illustrate their usefulness on the task of understanding executions of a leader election protocol.

This volume contains the proceedings of the 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), held at Reykjavik University in Iceland from 20 to 23 June 2017. LICS is an annual international forum on the broad range of topics that lie at the intersection of computer science and mathematical logic. In addition to the main symposium, seven workshops were co-located with LICS 2017: • INFINITY: Verification of Infinite-State Systems • LearnAut: Learning and Automata • LCC: Logic and Computational Complexit • LMW: Logic Mentoring Workshop • LOLA: Syntax and Semantics of Low-Level Languages • Metafinite model theory and definability and complexity of numeric graph parameters • WiL: Women in Logic

Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes., Comment: LMCS-2014-1018

Railway interlocking systems are apparatuses that prevent conflicting movements of trains through an arrangement of tracks. A railway interlocking system takes into consideration the position of the switches (of the turnouts) and only allows trains to be given clear signals if the routes to be used by the trains are disjoint. There are many different approaches to automate decision making in railway interlocking systems (i.e., to automate supervising that the proposed situation is safe). Meanwhile the classic approaches are offline: only certain routes are allowed and their compatibility is decided in advance, our approaches take the decision on real time, so performance is key. We had previously developed Maple implementations of models based on matrix, algebraic (Grobner bases), logic and logic–algebraic approaches. They are independent from the topology of the layout and can be applied to small or medium size layouts. In this paper another completely new model (also independent from the topology of the layout), that directly translates the decision problem into logic programming, is presented. This new approach directly translates the problem in answer set programming (ASP) style, by defining relations and derived relations, from which the problem is solved using logic techniques inherent to ASP. The main procedure analyses the safety of a proposed situation and an auxiliary procedure returns, if they exist, the sections where a collision could take place. This declarative approach turns out to be much faster and efficient than the previous ones by these authors, and therefore can be applied to much bigger layouts.

The majority of modern systems exhibit sophisticated concurrent behaviour, where several system components modify and observe the system state with fine-grained atomicity. Many systems (e.g., multi-core processors, real-time controllers) also exhibit truly concurrent behaviour, where multiple events can occur simultaneously. This paper presents data refinement defined in terms of an interval-based framework, which includes high-level operators that capture non-deterministic expression evaluation. By modifying the type of an interval, our theory may be specialised to cover data refinement of both discrete and continuous systems. We present an interval-based encoding of forward simulation, then prove that our forward simulation rule is sound with respect to our data refinement definition. A number of rules for decomposing forward simulation proofs over both sequential and parallel composition are developed., Comment: In Proceedings Refine 2013, arXiv:1305.5634

We design learning algorithms for synthesizing invariants using Horn implication counterexamples (Horn-ICE), extending the ICE-learning model. In particular, we describe a decision-tree learning algorithm that learns from nonlinear Horn-ICE samples, works in polynomial time, and uses statistical heuristics to learn small trees that satisfy the samples. Since most verification proofs can be modeled using nonlinear Horn clauses, Horn-ICE learning is a more robust technique to learn inductive annotations that prove programs correct. Our experiments show that an implementation of our algorithm is able to learn adequate inductive invariants and contracts efficiently for a variety of sequential and concurrent programs.

We study countably infinite MDPs with parity objectives, and special cases with a bounded number of colors in the Mostowski hierarchy (including reachability, safety, Büchi and co-Büchi). In finite MDPs there always exist optimal memoryless deterministic (MD) strategies for parity objectives, but this does not generally hold for countably infiniteMDPs. In particular, optimal strategies need not exist. For countable infinite MDPs, we provide a complete picture of the memory requirements of optimal (resp., ǫ-optimal) strategies for all objectives in the Mostowski hierarchy. In particular, there is a strong dichotomy between two different types of objectives. For the first type, optimal strategies, if they exist, can be chosen MD, while for the second type optimal strategies require infinite memory. (I.e., for all objectives in the Mostowski hierarchy, if finite-memory randomized strategies suffice then also MD-strategies suffice.) Similarly, some objectives admit ǫ-optimal MD-strategies, while for others ǫ-optimal strategies require infinite memory. Such a dichotomy also holds for the subclass of countably infinite MDPs that are finitely branching, though more objectives admit MD-strategies here.

First-order logic (FOL) is evidently insufficient for the many applications of logic in computer science, mainly due to its inability to provide inductive definitions. Therefore, only an extension of FOL which allows finitary inductive definitions can be used as a framework for automated reasoning. The minimal logic that is suitable for this goal is Ancestral Logic (AL), which is an extension of FOL by a transitive closure operator. In order for AL to be able to serve as a reasonable (and better) substitute to the use of FOL in computer science, it is crucial to develop adequate, user-friendly proof systems for it. While the expressiveness of AL renders any effective proof system for it incomplete with respect to the standard semantics, there are useful approximations. In this paper we show that such a Gentzen-style approximation is both sound and complete with respect to a natural, computationally-meaningful Henkin-style semantics for AL.

This paper introduces the idea of reactive semantics and reactive Beth tableaux for modal logic and quotes some of its applications. The reactive idea is very simple. Given a system with states and the possibility of transitions moving from one state to another, we can naturally imagine a path beginning at an initial state and moving along the path following allowed transitions. If our starting point is s 0, and the path is s 0, s 1,..., s n , then the system is ordinary non-reactive system if the options available at s n (i.e., which states t we can go to from s n ) do not depend on the path s 0,..., s n (i.e., do not depend on how we got to s n ). Otherwise if there is such dependence then the system is reactive. It seems that the simple idea of taking existing systems and turning them reactive in certain ways, has many new applications. The purpose of this paper is to introduce reactive tableaux in particular and illustrate and present some of the applications of reactivity in general. Mathematically one can take a reactive system and turn it into an ordinary system by taking the paths as our new states. This is true but from the point of view of applications there is serious loss of information here as the applicability of the reactive system comes from the way the change occurs along the path. In any specific application, the states have meaning, the transitions have meaning and the paths have meaning. Therefore the changes in the system as we go along a path can have very important meaning in the context, which enhances the usability of the model.

Marta Kwiatkowska is a Professor of Computing Systems and a Fellow of Trinity College at the University of Oxford. Before joining the University of Oxford, she was Professor in the School of Computer Science at the University of Birmingham, Lecturer at the University of Leicester and Assistant Professor at the Jagiellonian University in Cracow, Poland. She holds a BSc/MSc in Computer Science from the Jagiellonian University, an MA from Oxford and a PhD from the University of Leicester. In 2014, she was awarded an honorary doctorate from KTH Royal Institute of Technology in Stockholm and she became an ACM Fellow in 2016. Marta Kwiatkowska has been a pioneer in the development of model checking for probabilistic and quantitative systems. She was one the proposers of the use of multiterminal binary decision diagrams for the symbolic analysis of probabilistic systems and has done fundamental work on many of the models of quantitative systems that have been studied in the literature, such as continuous time Markov chains, Markov decision processes and stochastic games, amongst others. A hallmark of Marta Kwiatkowska's research career has been the synthesis of innovative and rigorous theoretical work with significant real-world applications. In addition, she has the ability to forge successful research connections with scientists from other sciences. She has led the development of the highly influential PRISM model checker 1 , recognised through the HVC 2016 Award, and has identified applications of quantitative verification to a wide range of areas, including security protocols, nanotechnology designs, power management, planning, and systems biology. In the past few years she has focused on applying quantitative techniques to the verification of pervasive and ubiquitous computing through her ERC Advanced Grant VERIWARE "From software verification to everyware verification" In addition to her outstanding research achievements, Marta Kwiatkowska has served the theoretical computer science community by sitting on prestigious award committees, organizing conferences and workshops and, perhaps even more importantly, by acting as an inspiring mentor for young researchers and as a role model for female researchers in computer science, to whom she has provided support and guidance. To wit, Marta Kwiatkowska has been the Senior Member of OxWoCS (Oxford Women in Computer Science Society) since its foundation in 2013 and has been a source of continued support and encouragement for that student-led society, providing its leadership with advice and suggestions for events as well as mentoring OxWoCS Committee members. Another interesting initiative for women with which she was involved is Suffrage Science 2 , which deserves to be advertised more broadly (not least because it involves jewellery designs). In addition to being named as ACM Fellow for "contributions to the theory and practice of probabilistic verification", Marta Kwiatkowska is a member of Academia Europea and a Fellow of the British Computer Society. She is a true stalwart of the Logic in Computer Science research community and a great example for young researchers. It is therefore fitting to spotlight her contribution in this column of ACM SIGLOG News.

Hybrid temporal logic (HTL) on data words can be considered as an extension of the logic LTL^@7 introduced by Demri and Lazic [Stephane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. In LICS@?06: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, pages 17-26, Washington, DC, USA, 2006. IEEE Computer Society]. The paper compares the expressive power of HTL on data words with that of LTL^@7. It is shown that there are properties of data words that can be expressed in HTL with two variables but not in LTL^@7. On the other hand, every property that can be expressed in HTL with one variable can also be expressed in LTL^@7 with one variable. The paper further studies the succinctness of HTL in comparison with LTL^@7 and shows that the number-of-variables hierarchy of HTL is infinite.

We introduce a new nameless representation of lambda terms inspired by ordered logic. At a lambda abstraction, number and relative position of all occurrences of the bound variable are stored, and application carries the additional information where to cut the variable context into function and argument part. This way, complete information about free variable occurrence is available at each subterm without requiring a traversal, and environments can be kept exact such that they only assign values to variables that actually occur in the associated term. Our approach avoids space leaks in interpreters that build function closures. In this article, we prove correctness of the new representation and present an experimental evaluation of its performance in a proof checker for the Edinburgh Logical Framework. Keywords: representation of binders, explicit substitutions, ordered contexts, space leaks, Logical Framework., Comment: In Proceedings LFMTP 2011, arXiv:1110.6685

Abramsky and Coecke (Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 415–425, IEEE Comput. Soc., New York, 2004) have recently introduced an approach to finite dimensional quantum mechanics based on strongly compact closed categories with biproducts. In this note it is shown that the projections of any object A in such a category form an orthoalgebra Proj A. Sufficient conditions are given to ensure this orthoalgebra is an orthomodular poset. A notion of a preparation for such an object is given by Abramsky and Coecke, and it is shown that each preparation induces a finitely additive map from Proj A to the unit interval of the semiring of scalars for this category. The tensor product for the category is shown to induce an orthoalgebra bimorphism Proj A×Proj B→Proj (A⊗B) that shares some of the properties required of a tensor product of orthoalgebras.

We use the Edit distance with Moves on words and trees and say that two regular (tree) languages are ?-close if every word (tree) of one language is ?-close to the other. A transducer model is introduced to compare tree languages (schemas) with different alphabets and attributes. Using the statistical embedding of Fischer et al. (Proceedings of 21st IEEE Symposium on Logic in Computer Science, pp. 421---430, 2006), we show that Source-Consistency and Approximate Query Answering are testable on words and trees, i.e. can be approximately decided within ? by only looking at a constant fraction of the input.

Even when a system is proven to be correct with respect to a specification, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. Coverage metrics attempt to check which parts of a system are actually relevant for the verification process to succeed. Recent work on coverage in model checking suggests several coverage metrics and algorithms for finding parts of the system that are not covered by the specification. The work has already proven to be effective in practice, detecting design errors that escape early verification efforts in industrial settings. In this article, we relate a formal definition of causality given by Halpern and Pearl to coverage. We show that it gives significant insight into unresolved issues regarding the definition of coverage and leads to potentially useful extensions of coverage. In particular, we introduce the notion of responsibility , which assigns to components of a system a quantitative measure of their relevance to the satisfaction of the specification.

We report complexity results about redundancy of formulae in 2CNF form. We first consider the problem of checking redundancy and show some algorithms that are slightly better than the trivial one. We then analyze problems related to finding irredundant equivalent subsets (I.E.S.) of a given set. The concept of cyclicity proved to be relevant to the complexity of these problems. Some results about Horn formulae are also shown., Comment: Corrected figures on Theorem 10; added and modified some references

Logical frameworks serve as meta languages to represent deductive systems, sometimes requiring special purpose meta logics to reason about the representations. In this work, we describe L"@w^+, a meta logic for the linear logical framework LLF [Iliano Cervesato and Frank Pfenning. A linear logical framework. In E. Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, pages 264-275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.] and illustrate its use via a proof of the admissibility of cut in the sequent calculus for the tensor fragment of linear logic. L"@w^+ is first-order, intuitionistic, and not linear. The soundness of L"@w^+ is shown.

The probability logic denoted \(LPP_2\) is described with the aim to give a clear, step-by-step introduction to the field and the main proof techniques that will be used elsewhere in the book. The logic enriches propositional calculus with probabilistic operators of the form \(P_{\ge s}\) with the intended meaning “probability is at least s”. In \(LPP_2\) the operators are applied to propositional formulas, while iterations of probability operators are not allowed. Possible world semantics with a finitely additive probability measure on sets of worlds definable by formulas is defined, so that formulas remain true or false. The corresponding axiomatization is provided. The axiom system is infinitary. It contains an infinitary rule with countable many premisses and one conclusion. The rule is related to the Archimedean property of real numbers. The logic \(LPP_2\) is not compact: there are unsatisfiable sets of formulas that are finitely satisfiable. Some of the consequences of non-compactness are described. Then, soundness and strong completeness of the logic is proved with respect to several classes of probability models. This is followed by a proof of decidability of PSAT, the satisfiability problem for \(LPP_2\), which is NP-complete. Finally, a heuristic approach to PSAT is presented. This Chapter covers some results from Ikodinovic et al., Int J Approx Reason, (55):1830–1842, 2014, [3], Jovanovic et al., Variable neighborhood search for the probabilistic satisfiability problem, 2007, [4], Kokkinis et al., Logic J. IGPL, (23):662–687, 2015, [5], Ognjanovic, J. Logic Comput, (9):181–195, 1999, [6], Ognjanovic et al., Theor Comput Sci, (247):191–212, 2000, [7], Ognjanovic et al., A genetic algorithm for satisfiability problem in a probabilistic logic, 2001, [8],Ognjanovic et al., A Genetic Algorithm for Probabilistic SAT Problem, 2004, [9], Ognjanovic et al., A Hybrid Genetic and Variable Neighborhood Descent for Probabilistic SAT Problem, 2005, [10], Ognjanovic et al., Zbornik Radova, Subseries Logic in Computer Science, 2009, [11], Raskovic and Ognjanovic, Some propositional probabilistic logics, 1996, [12], Raskovic and Ognjanovic, A first order probability logic, \(LP_Q\), 1999, [13], Stojanovic et al., Appl Soft Comput, (31):339–347, 2015, [14].

The first order probability logic \({ LFOP}_{1}\) is introduced. The logic allows formulas about higher-order probabilities. To give semantics to the logic we introduced first order probability models with constant domains and rigid terms. An infinitary axiom system for \({ LFOP}_{1}\) is presented. The logic \({ LFOP}_{1}\) inherits the main properties of \(LPP_2\), so, in spite of all differences, we use the techniques from Chap. 3 to prove strong completeness. The same technique can be also applied to other kinds of probability logics: the first order \({ LFOP}_2\), and propositional \({ LPP}_1\), etc. In \({ LFOP}_{1}\)-formulas probabilistic operators and the classical quantifiers can be mixed and nested, so the logic is related to modal logics and we discuss how (translations of) some properties of modal logics (e.g., Barcan formula) behave in the probabilistic settings. Since \({ LFOP}_{1}\) extends classical first order logic, it is undecidable, but we show that the monadic fragment of \({ LFOP}_{1}\) without iterations of probability operators is decidable. The same hold for the propositional \({ LPP}_1\). Finally, the logic \({ LPP}_1^{\mathrm {LTL}}\) suitable for a combination of probability and temporal reasoning is presented. This chapter covers some results from Ikodinovic, Proceedings of the 8th European conference symbolic and quantitative approaches to reasoning with uncertainty ECSQARU 2005, vol 3571, pp 726–736, 2005, [10], Markovic et al. Int J Approx Reason, 49(1): 52–66, 2008, [11], Milosevic, Ognjanovic, Logic J Interes Group Pure Appl Logics, 20(1): 235–253, 2012, [12], Milosevic, Ognjanovic, Publications de L’InstituteMatematique, ns, 93(107): 19–27, 2013, [8], Ognjanovic, J Logic Comput 16(2): 257–285, 2006, [15], Ognjanovic, Publications de L’Institute Matematique (Beograd), ns, 82(96): 141–154, 2007, [16], Ognjanovic, Raskovic, Publications de L’Institute Matematique (Beograd), ns, 60(74): 1–4, 1996, [13], Ognjanovic, Raskovic, Theor Comput Sci, 247(1–2): 191–212, 2000, [14], Ognjanovic et al. Fifth international conference on scalable uncertainty management SUM-2011, vol 6929, pp 219–232, 2011, [18], Ognjanovic et al. Zbornik radova. Subseries logic in computer science, vol 12(20), pp 35-111, [17], Perovic et al. Proceedings of the 5th international symposium foundations of information and knowledge systems FoIKS 2008, vol 4932, pp 239–252, 2008, [21], Raskovic, Ognjanovic, Proceedings of the Kurepa’s symposium 1996, pp 83–90, 1996, [19].

Priced timed automata provide a natural model for quantitative analysis of real-time systems and have been successfully applied in various scheduling and planning problems. The optimal reachability problem for linearly-priced timed automata is known to be PSPACE-complete. In this paper we investigate priced timed automata with more general prices and show that in the most general setting the optimal reachability problem is undecidable. We adapt and implement the construction of Audemard, Cimatti, Kornilowicz, and Sebastiani for non-linear priced timed automata using state-of-the-art theorem prover Z3 and present some preliminary results., Comment: In Proceedings V2CPS-16, arXiv:1612.04023

We pursue the program of exposing the intrinsic mathematical structure of the ''space of proofs'' of a logical system [S. Abramsky and R. Jagadeesan. Games and Full Completeness for Multiplicative Linear Logic, Journal of Symbolic Logic, (1994), vol. 59, no. 2, 543–574]. We study the case of Multiplicative-Additive Linear Logic (MALL). We use tools from Domain theory to develop a semantic notion of proof net for MALL, and prove a Sequentialization Theorem. This work forms part of a continuation of previous joint work with Radha Jagadeesan [S. Abramsky and R. Jagadeesan. Games and Full Completeness for Multiplicative Linear Logic, Journal of Symbolic Logic, (1994), vol. 59, no. 2, 543–574] and Paul-André Melliès [S. Abramsky and P.-A. Melliès. Concurrent Games and Full Completeness. Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 431–44, 1999].

Nominal sets provide a mathematical theory for some of the key concepts that arise when representing and computing with data involving atomic (or 'pure') names: freshness, abstraction and scoping of names, and finiteness modulo symmetry. This tutorial introduces the notion of nominal set and explains selected applications of it to logic in computer science, to automata, languages and programming.

Separation logic [Reynolds, J. C., Intuitionistic reasoning about shared mutable data structure, in: J. Davies, B. Roscoe and J. Woodcock, editors, Millennial Perspectives in Computer Science, Palgrave, 2000 pp. 303–321; Reynolds, J. C., Separation logic: A logic for shared mutable data structures, in: LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (2002), pp. 55–74; O'Hearn, P., J. Reynolds and H. Yang, Local reasoning about programs that alter data structures, in: L. Fribourg, editor, CSL 2001 (2001), pp. 1–19, LNCS 2142] began life as an extended formalisation of Burstall's treatment of list-mutating programs [Burstall, R., Some techniques for proving correctness of programs which alter data structures, Machine Intelligence 7 (1972), pp. 23–50]. It rapidly became clear that there was more that it could say: O'Hearn's discovery [O'Hearn, P., Notes on separation logic for shared-variable concurrency (2002), unpublished] of ownership transfer of buffers between threads and Boyland's suggestion [Boyland, J., Checking interference with fractional permissions, in: R. Cousot, editor, Static Analysis: 10th International Symposium, Lecture Notes in Computer Science 2694 (2003), pp. 55–72] of permissions to deal with variable and heap sharing pointed the way to a treatment of safe resource management in concurrent programs. That treatment has so far been incomplete because it deals only with heap cells and not with with (stack) variables as resource. Adding variable contexts' — in the simplest case, lists of owned variables — to assertions in Hoare logic allows a resource treatment of variables. It seems that a formal treatment of aliasing is possible too. It gives a complete formal treatment of critical sections (for the first time, so far as I am aware).

We present domain-theoretic models that support both probabilistic and nondeterministic choice. In [A. McIver and C. Morgan. Partial correctness for probablistic demonic programs. Theoretical Computer Science, 266:513-541, 2001], Morgan and McIver developed an ad hoc semantics for a simple imperative language with both probabilistic and nondeterministic choice operators over a discrete state space, using domain-theoretic tools. We present a model also using domain theory in the sense of D.S. Scott (see e.g. [G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. W. Mislove, and D. S. Scott. Continuous Lattices and Domains, volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 2003]), but built over quite general continuous domains instead of discrete state spaces. Our construction combines the well-known domains modelling nondeterminism - the lower, upper and convex powerdomains, with the probabilistic powerdomain of Jones and Plotkin [C. Jones and G. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 186-195. IEEE Computer Society Press, 1989] modelling probabilistic choice. The results are variants of the upper, lower and convex powerdomains over the probabilistic powerdomain (see Chapter 4). In order to prove the desired universal equational properties of these combined powerdomains, we develop sandwich and separation theorems of Hahn-Banach type for Scott-continuous linear, sub- and superlinear functionals on continuous directed complete partially ordered cones, endowed with their Scott topologies, in analogy to the corresponding theorems for topological vector spaces in functional analysis (see Chapter 3). In the end, we show that our semantic domains work well for the language used by Morgan and McIver.

I would like to start my tenure as editor of the Logic Column by thanking Jon Riecke, who has edited this column since 1998. The Logic Column serves as a showcase of the many connections between logic and computer science. Logic has been connected with computer science since the early days of Turing. In the past few decades, logical methods have had a considerable impact. To get a sense of the range of applications, consider the 2001 NSF/CISE Workshop on The Unusual Effectiveness of Logic in Computer Science (see http: //www. cs. rice. edu/~vardi/logic/). An article derived from the workshop appeared in the Bulletin of Symbolic Logic [Halpern et al. 2001], and it is an exceedingly good read. If you get a copy of that issue of the Bulletin, make sure to also have a look at the article by Buss et al. [2001], which discusses the current state of mathematical logic.

We present the class of binary automaton, a new representation for the subsets of N m that naturally extends the NDD ([Wolper, P. and B. Boigelot, An automata-theoretic approach to Presburger arithmetic constraints, in: Proc. 2nd Int. Symp. Static Analysis (SAS'95), Glasgow, UK, Sep. 1995, Lecture Notes in Computer Science 983 (1995), pp. 21–32], [Boudet, A. and H. Comon, Diophantine equations, Presburger arithmetic and finite automata, in: Proc. 21st Int. Coll. on Trees in Algebra and Programming (CAAP'96), Linkoping, Sweden, Apr. 1996, Lecture Notes in Computer Science 1059 (1996), pp. 30–43]). We prove that the affine hull of the set of vectors represented by a binary automaton is computable in polynomial time. As application, we show that the set of place invariants [Ciardo, G., Petri nets with marking-dependent arc cardinality: Properties and analysis, in: Proc. 15th Int. Conf. Application and Theory of Petri Nets (ICATPN'94), Zaragoza, Spain, June 1994, Lecture Notes in Computer Science 815 (1994), pp. 179–198] of a counter system (an extension of the Broadcast Protocols [Emerson, E. A. and K. S. Namjoshi, On model checking for non-deterministic infinite-state systems, in: Proc. 13th IEEE Symp. Logic in Computer Science (LICS'98), Indianapolis, IN, USA, June 1998 (1998), pp. 70–80], [Delzanno, G., Verification of consistency protocols via infinite-state symbolic model checking: A case study, in: Proc. IFIP Joint Int. Conf. Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV'00), Pisa, Italy, Oct. 2000, IFIP Conference Proceedings 183 (2000), pp. 171–186], [Delzanno, G., Constraint-based verification of parameterized cache coherence protocols, Formal Methods in System Design. To appear], the Reset/Transfer Petri Nets [Dufourd, C., A. Finkel and P. Schnoebelen, Reset nets between decidability and undecidability, in: Proc. 25th Int. Coll. Automata, Languages, and Programming (ICALP'98), Aalborg, Denmark, July 1998, Lecture Notes in Computer Science 1443 (1998), pp. 103–115], [Ciardo, G., Petri nets with marking-dependent arc cardinality: Properties and analysis, in: Proc. 15th Int. Conf. Application and Theory of Petri Nets (ICATPN'94), Zaragoza, Spain, June 1994, Lecture Notes in Computer Science 815 (1994), pp. 179–198] and the linear systems [Finkel, A. and J. Leroux, How to compose Presburger-accelerations: Applications to broadcast protocols, in: Proc. 22nd Conf. Found. of Software Technology and Theor. Comp. Sci. (FST&TCS'2002), Kanpur, India, Dec. 2002, Lecture Notes in Computer Science 2556 (2002), pp. 145–156]), is computable in polynomial time.

Partial metrics, or the equivalent weightable quasi-metrics, have been introduced in Matthews (Proc. 8th Summer Conf. on General Topology and Applications; Ann. New York Acad. Sci. 728 (1994) 183) as part of the study of the denotational semantics of data flow networks (Theoret. Comput. Sci. 151 (1995) 195). The interest in valuations in connection to Domain Theory derives from e.g. Jones and Plotkin (LICS ’89, IEEE Computer Society Press, Silver Spring, MD, 1998, pp. 186–195), Jones (Ph.D. Thesis, University of Edinburgh, 1989), Edalat (LICS’94, IEEE Computer Society Press, Silver Spring, MD, 1994) and Heckmann (Fund. Inform. 24(3) (1995) 259). Connections between partial metrics and valuations have been discussed in the literature, e.g. O'Neill (in: S. Andima et al. (Eds.), Proc. 11th Summer Conf. on General Topology and Applications; Ann. New York Acad. Sci. 806 (1997) 304), Bukatin and Scott (in: S. Adian, A. Nerode (Eds.), Logical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 1234, Springer, Berlin, 1997, pp. 33–43) and Bukatin and Shorina (in: M. Nivat (Ed.), Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Vol. 1378, Springer, Berlin, 1998, pp. 125–139). In each case, partial metrics are generated from strictly increasing valuations.We analyze the precise relationship between these two notions. It is well known that characterizations of partial metrics in general are hard to obtain, as witnessed by the open characterization problems in the survey paper Nonsymmetric Topology (Kúnzi (Bolyai Soc. Math. Stud. 4 (1993) 303). Our approach to obtaining such a characterization involves the isolation of a “mathematically nice” class of spaces, which is sufficiently large to incorporate the quantitative domain theoretic examples involving partial metric spaces.For these purposes we focus on the class of quasi-metric semilattices. These structures, as will be illustrated, arise naturally in quantitative domain theory and include in particular the class of totally bounded Scott domains discussed in Smyth (in: G.M. Reed, A.W. Roscoe, R.F. Wachter (Ed.), Topology and Category Theory in Computer Science, Oxford University Press, Oxford, 1991, pp. 207–229), the Baire quasi-metric spaces of (Theoret. Comput. Sci. 151 (1995) 195), the complexity spaces of Schellekens (in: Proc. MFPS 11, Electronic Notes in Theoretical Computer Science, Vol. I, Elsevier, Amsterdam, 1995, pp. 211–232) and the interval domain (Proc. Twelfth Ann. IEEE Symp. on Logic in Computer Science, IEEE Press, New York, 1997, pp. 248–257).We introduce the notion of a semivaluation, which generalizes the fruitful notion of a valuation on a lattice to the context of semilattices and establish a correspondence between partial metric semilattices and semivaluation spaces.

The Autoepistemic Logic of Knowledge and Belief (AELB) is a powerful nonmonotic formalism introduced by Teodor Przymusinski in 1994. In this paper, we specialize it to a class of theories called `super logic programs'. We argue that these programs form a natural generalization of standard logic programs. In particular, they allow disjunctions and default negation of arbibrary positive objective formulas. Our main results are two new and powerful characterizations of the static semant ics of these programs, one syntactic, and one model-theoretic. The syntactic fixed point characterization is much simpler than the fixed point construction of the static semantics for arbitrary AELB theories. The model-theoretic characterization via Kripke models allows one to construct finite representations of the inherently infinite static expansions. Both characterizations can be used as the basis of algorithms for query answering under the static semantics. We describe a query-answering interpreter for super programs which we developed based on the model-theoretic characterization and which is available on the web., 47 pages, revised version of the paper submitted 10/2000

In this paper we consider first-order logic theorem proving and model building via approximation and instantiation. Given a clause set we propose its approximation into a simplified clause set where satisfiability is decidable. The approximation extends the signature and preserves unsatisfiability: if the simplified clause set is satisfiable in some model, so is the original clause set in the same model interpreted in the original signature. A refutation generated by a decision procedure on the simplified clause set can then either be lifted to a refutation in the original clause set, or it guides a refinement excluding the previously found unliftable refutation. This way the approach is refutationally complete. We do not step-wise lift refutations but lift conflicting cores, finite unsatisfiable clause sets representing at least one refutation. The approach is dual to many existing approaches in the literature.

This paper introduces HHL, a hierarchical variant of hybrid logic. First-order correspondence and a Hennessy-Milner like theorem relating (hierarchical) bisimulation and logical equivalence for HHLare presented. Combining hierarchical transition structures with the ability to refer to specific states at any level of description, this logic seems suitable to express and verify properties of hierarchical transition systems, a pervasive semantic structure in Computer Science., Dynamic logic combines logic with programs, which at a certain level of abstraction, can be regarded as behaviours changing the system state and, therefore, the truth value of formulas. This paper suggests a method for generating such logics for the domain of robot controllers and illustrates it with a logic for handling resource consumption.

Anuj Dawar poses two questions which give finitary analogies to the Lowenheim–Skolem theorems. Grohe (Proc. of the 12th IEEE Symp. on Logic in Computer Science, 1997), has shown that the first of these, which corresponds to the downward Lowenheim–Skolem theorem, has a negative answer. In this paper we combine Grohe's technique with that of Robinson's famous paper (Trans. Amer. Math. Soc. (1952)) to show that the second question, which corresponds to the upward Lowenheim–Skolem theorem, also has a negative answer.

We investigate the power of first-order logic with only two variables overomega-words and finite words, a logic denoted by FO2. We prove that FO2 canexpress precisely the same properties as linear temporal logic with only the unary temporal operators: “next”, “previously”, “sometime in the future”, and “sometime in the past”, a logic we denote by unary-TL. Moreover, our translation from FO2 to unary-TL converts every FO2 formula to an equivalent unary-TL formula that is at most exponentially larger, and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is optimal.While satisfiability for full linear temporal logic, as well as forunary-TL, is known to be PSPACE-complete, we prove that satisfiabilityfor FO2 is NEXP-complete, in sharp contrast to the fact that satisfiabilityfor FO3 has non-elementary computational complexity. Our NEXP timeupper bound for FO2 satisfiability has the advantage of being in terms ofthe quantifier depth of the input formula. It is obtained using a small model property for FO2 of independent interest, namely: a satisfiable FO2 formula has a model whose “size” is at most exponential in the quantifier depth of the formula. Using our translation from FO2 to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.

In this paper, we investigate several extensions of the linear time hierarchy (denoted by LTH). We first prove that it is not necessary to erase the oracle tape between two successive oracle calls, thereby lifting a common restriction on LTH machines. We also define a natural counting extension of LTH and show that it corresponds to a robust notion of counting bounded arithmetic predicates. Finally, we show that the computational power of the majority operator is equivalent to that of the exact counting operator in both contexts.

Communication présentée au "3rd International Conference on Predictive Modelling in Foods, Leuven, Belgium12–15 September 2000"; Various predictive models of microbial behavior have been created and extensive data collection has been done by numerous private or public laboratories. However, significant differences between predicted and observed values in foods have been observed and need to be stressed, understood and explained as much as possible. In this paper, we present a software tool (currently at the level of a prototype) able: (i) to store in a database all relevant information expressed on one hand as qualitative or quantitative data and on the other hand as precise or imprecise data; (ii) to retrieve the more relevant information from the database using queries where criteria may be expressed as fuzzy values in order to enhance the flexibility of the search; (iii) to compute, in addition to the nearest data, an estimation of searched values using statistical models. The architecture of this software tool is structured as a category-based reasoning system. Example queries about Listeria monocytogenes (L. monocytogenes) illustrate the functionalities of this tool.

To acknowledge the long-term, foundational nature of papers appearing in LICS, the Test-of-Time Award is now awarded every year to the paper or papers that were published in LICS twenty years ago and that have "stood the test of time." The Test-of-Time Award Committee consisting of Christel Baier, Amy Felty (chair), Andrew Pitts and Nicole Schweikardt made two awards in 2017 to honor outstanding papers from the 12th IEEE Symposium on Logic in Computer Science, held 1997 in Warsaw, Poland

We study the descriptive complexity of parity games by taking into account the coloring of their game graphs whilst ignoring their ownership structure. Colorings of game graphs are identified if they determine the same winning regions and strategies, for all ownership structures of nodes. The Rabin index of a parity game is the minimum of the maximal color taken over all equivalent coloring functions. We show that deciding whether the Rabin index is at least k is in P for k=1 but NP-hard for all fixed k≥2. We present an EXPTIME algorithm that computes the Rabin index by simplifying its input coloring function. When replacing simple cycle with cycle detection in that algorithm, its output over-approximates the Rabin index in polynomial time. We evaluate this efficient algorithm as a preprocessor of solvers in detailed experiments: for Zielonka's solver on random and structured parity games and for our partial solver psolB on random games.