Logic in Computer Science
New submissions
[ showing up to 2000 entries per page: fewer  more ]
New submissions for Thu, 19 May 22
 [1] arXiv:2205.08572 [pdf, other]

Title: Building Information Modeling Using Constraint Logic ProgrammingComments: Paper presented at the 38th International Conference on Logic Programming (ICLP 2022), 16 pagesSubjects: Logic in Computer Science (cs.LO)
Building Information Modeling (BIM) produces threedimensional models of buildings combining the geometrical information with a wide range of properties. BIM is slowly but inevitably revolutionizing the architecture, engineering, and construction (AEC) industry. Buildings need to be compliant with regulations about stability, safety, and environmental impact. Manual compliance checking is tedious and errorprone, and amending flaws discovered only at construction time causes huge additional costs and delays. Several tools can check BIM models for conformance with rules/guidelines. For example, Singapore's CORENET eSubmission System checks fire safety. But since the current BIM exchange format only contains basic information of building objects, a separate, adhoc model preprocessing is required to determine, e.g., evacuation routes. Moreover, they face difficulties in adapting existing builtin rules and/or adding new ones (to cater for building regulations, that can vary not only among countries but also among parts of the same city), if at all possible. We propose the use of logicbased executable formalisms (CLP and Constraint ASP) to couple BIM models with advanced knowledge representation and reasoning capabilities. Previous experience shows that such formalisms can be used to uniformly capture and reason with knowledge (including ambiguity) in a large variety of domains. Additionally, incorporating checking within design tools makes it possible to ensure that models are rulecompliant at every step. This also prevents erroneous designs from having to be (partially) redone, which is also costly and burdensome. To validate our proposal, we implemented a preliminary reasoner under CLP(Q/R) and ASP with constraints and evaluated it with several BIM models. Under consideration for acceptance in Theory and Practice of Logic Programming (TPLP).
 [2] arXiv:2205.08616 [pdf, ps, other]

Title: Cyclic Proofs, Hypersequents, and Transitive Closure LogicSubjects: Logic in Computer Science (cs.LO)
We propose a cutfree cyclic system for Transitive Closure Logic (TCL) based on a form of hypersequents, suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cutfree incomplete for basic validities from Kleene Algebra (KA) and Propositional Dynamic Logic (PDL), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and PDL, thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, exhibiting 'alternating traces' and necessitating a more intricate soundness argument than for traditional cyclic proofs.
 [3] arXiv:2205.08628 [pdf, ps, other]

Title: Mechanized Analysis of Anselm's Modal Ontological ArgumentAuthors: John RushbyJournalref: International Journal for Philosophy of Religion, vol. 89, pp. 135152, April 2021Subjects: Logic in Computer Science (cs.LO)
We use a mechanized verification system, PVS, to examine the argument from Anselm's Proslogion Chapter III, the socalled "Modal Ontological Argument." We consider several published formalizations for the argument and show they are all essentially similar. Furthermore, we show that the argument is trivial once the modal axioms are taken into account.
This work is an illustration of computational philosophy and, in addition, shows how these methods can help detect and rectify errors in modal reasoning.  [4] arXiv:2205.08632 [pdf, other]

Title: DPO: DynamicProgramming Optimization on Hybrid ConstraintsSubjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Data Structures and Algorithms (cs.DS)
In Bayesian inference, the most probable explanation (MPE) problem requests a variable instantiation with the highest probability given some evidence. Since a Bayesian network can be encoded as a literalweighted CNF formula $\varphi$, we study Boolean MPE, a more general problem that requests a model $\tau$ of $\varphi$ with the highest weight, where the weight of $\tau$ is the product of weights of literals satisfied by $\tau$. It is known that Boolean MPE can be solved via reduction to (weighted partial) MaxSAT. Recent work proposed DPMC, a dynamicprogramming model counter that leverages graphdecomposition techniques to construct projectjoin trees. A projectjoin tree is an execution plan that specifies how to conjoin clauses and project out variables. We build on DPMC and introduce DPO, a dynamicprogramming optimizer that exactly solves Boolean MPE. By using algebraic decision diagrams (ADDs) to represent pseudoBoolean (PB) functions, DPO is able to handle disjunctive clauses as well as XOR clauses. (Cardinality constraints and PB constraints may also be compactly represented by ADDs, so one can further extend DPO's support for hybrid inputs.) To test the competitiveness of DPO, we generate random XORCNF formulas. On these hybrid benchmarks, DPO significantly outperforms MaxHS, UWrMaxSat, and GaussMaxHS, which are stateoftheart exact solvers for MaxSAT.
 [5] arXiv:2205.08718 [pdf, ps, other]

Title: An approach to translating Haskell programs to Agda and reasoning about themSubjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL); Software Engineering (cs.SE)
We are using the Agda programming language and proof assistant to formally verify the correctness of a Byzantine Fault Tolerant consensus implementation based on HotStuff / LibraBFT. The Agda implementation is a translation of our Haskell implementation based on LibraBFT. This short paper focuses on one aspect of this work.
We have developed a library that enables the translated Agda implementation to closely mirror the Haskell code on which it is based. This makes it easier and more efficient to review the translation for accuracy, and to maintain the translated Agda code when the Haskell code changes, thereby reducing the risk of translation errors. We also explain how we capture the semantics of the syntactic features provided by our library, thus enabling formal reasoning about programs that use them; details of how we reason about the resulting Agda implementation will be presented in a future paper.
The library that we present is independent of our particular verification project, and is available, opensource, for others to use and extend.  [6] arXiv:2205.08869 [pdf, ps, other]

Title: Automatic Complexity Analysis of Integer Programs via Triangular Weakly NonLinear LoopsSubjects: Logic in Computer Science (cs.LO)
There exist several results on deciding termination and computing runtime bounds for triangular weakly nonlinear loops (twnloops). We show how to use results on such subclasses of programs where complexity bounds are computable within incomplete approaches for complexity analysis of full integer programs. To this end, we present a novel modular approach which computes local runtime bounds for subprograms which can be transformed into twnloops. These local runtime bounds are then lifted to global runtime bounds for the whole program. The power of our approach is shown by our implementation in the tool KoAT which analyzes complexity of programs where all other stateoftheart tools fail.
 [7] arXiv:2205.08920 [pdf, other]

Title: Finite twodimensional proof systems for nonfinitely axiomatizable logicsSubjects: Logic in Computer Science (cs.LO); Logic (math.LO)
The characterizing properties of a prooftheoretical presentation of a given logic may hang on the choice of proof formalism, on the shape of the logical rules and of the sequents manipulated by a given proof system, on the underlying notion of consequence, and even on the expressiveness of its linguistic resources and on the logical framework into which it is embedded. Standard (onedimensional) logics determined by (nondeterministic) logical matrices are known to be axiomatizable by analytic and possibly finite proof systems as soon as they turn out to satisfy a certain constraint of sufficient expressiveness. In this paper we introduce a recipe for cooking up a twodimensional logical matrix (or Bmatrix) by the combination of two (possibly partial) nondeterministic logical matrices. We will show that such a combination may result in Bmatrices satisfying the property of sufficient expressiveness, even when the input matrices are not sufficiently expressive in isolation, and we will use this result to show that onedimensional logics that are not finitely axiomatizable may inhabit finitely axiomatizable twodimensional logics, becoming, thus, finitely axiomatizable by the addition of an extra dimension. We will illustrate the said construction using a wellknown logic of formal inconsistency called mCi. We will first prove that this logic is not finitely axiomatizable by a onedimensional (generalized) Hilbertstyle system. Then, taking advantage of a known 5valued nondeterministic logical matrix for this logic, we will combine it with another one, conveniently chosen so as to give rise to a Bmatrix that is axiomatized by a twodimensional Hilbertstyle system that is both finite and analytic.
 [8] arXiv:2205.08952 [pdf, ps, other]

Title: Zigzag normalisation for associative $n$categoriesJournalref: Proceedings of the ThirtySeventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022)Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)
The theory of associative $n$categories has recently been proposed as a strictly associative and unital approach to higher category theory. As a foundation for a proof assistant, this is potentially attractive, since it has the potential to allow simple formal proofs of complex highdimensional algebraic phenomena. However, the theory relies on an implicit term normalisation procedure to recognize correct composites, with no recursive method available for computing it.
Here we describe a new approach to term normalisation in associative $n$categories, based on the categorical zigzag construction. This radically simplifies the theory, and yields a recursive algorithm for normalisation, which we prove is correct. Our use of categorical lifting properties allows us to give efficient proofs of our results. This normalisation algorithm forms a core component of the proof assistant homotopy.io, and we illustrate our scheme with worked examples.  [9] arXiv:2205.08976 [pdf, ps, other]

Title: CTL* model checking for dataaware dynamic systems with arithmeticComments: arXiv admin note: text overlap with arXiv:2203.07982Subjects: Logic in Computer Science (cs.LO)
The analysis of complex dynamic systems is a core research topic in formal methods and AI, and combined modelling of systems with data has gained increasing importance in applications such as business process management. In addition, process mining techniques are nowadays used to automatically mine process models from event data, often without correctness guarantees. Thus verification techniques for linear and branching time properties are needed to ensure desired behavior. Here we consider dataaware dynamic systems with arithmetic (DDSAs), which constitute a concise but expressive formalism of transition systems with linear arithmetic guards. We present a CTL* model checking procedure for DDSAs that relies on a finitestate abstraction by means of a set of formulas that capture variable configurations. Lineartime verification was shown to be decidable in specific classes of DDSAs where the constraint language or the control flow are suitably confined. We investigate several of these restrictions for the case of CTL*, with both positive and negative results: CTL* verification is proven decidable for monotonicity and integer periodicity constraint systems, but undecidable for feedback free and bounded lookback systems. To demonstrate the feasibility of our approach, we implemented it in the SMTbased prototype ada, showing that many practical business process models can be effectively analyzed.
 [10] arXiv:2205.08988 [pdf, other]

Title: Formalization of Advanced VOs semantics and VO RefinementAuthors: Sebastian Stock, Fabian Vu, David Geleßus, Atif Mashkoor, Michael Leuschel, Alexander EgyedSubjects: Logic in Computer Science (cs.LO)
This document lays out the foundations for VO and requirement refinement, abstractions of models, and instantiations. Also, VOs on abstractions and instantiations are considered.
 [11] arXiv:2205.09015 [pdf, ps, other]

Title: Ramsey Quantifiers over Automatic Structures: Complexity and Applications to VerificationSubjects: Logic in Computer Science (cs.LO)
Automatic structures are infinite structures that are finitely represented by synchronized finitestate automata. This paper concerns specifically automatic structures over finite words and trees (ranked/unranked). We investigate the "directed version" of Ramsey quantifiers, which express the existence of an infinite directed clique. This subsumes the standard "undirected version" of Ramsey quantifiers. Interesting connections between Ramsey quantifiers and two problems in verification are firstly observed: (1) reachability with B\"{u}chi and generalized B\"{u}chi conditions in regular model checking can be seen as Ramsey quantification over transitive automatic graphs (i.e., whose edge relations are transitive), (2) checking monadic decomposability (a.k.a. recognizability) of automatic relations can be viewed as Ramsey quantification over cotransitive automatic graphs (i.e., the complements of whose edge relations are transitive). We provide a comprehensive complexity landscape of Ramsey quantifiers in these three cases (general, transitive, cotransitive), all between NL and EXP. In turn, this yields a wealth of new results with precise complexity, e.g., verification of subtree/flat prefix rewriting, as well as monadic decomposability over treeautomatic relations. We also obtain substantially simpler proofs, e.g., for NL complexity for monadic decomposability over wordautomatic relations (given by DFAs).
 [12] arXiv:2205.09082 [pdf, other]

Title: Realizability Checking of Contracts with Kind 2Subjects: Logic in Computer Science (cs.LO)
We present a new feature of the opensource model checker Kind 2 which checks whether a component contract is realizable; i.e., it is possible to construct a component such that for any input allowed by the contract assumptions, there is some output value that the component can produce that satisfies the contract guarantees. When the contract is proven unrealizable, it provides a deadlocking computation and a set of conflicting guarantees. This new feature can be used to detect flaws in component specifications and to ensure the correctness of Kind 2's compositional proof arguments.
Crosslists for Thu, 19 May 22
 [13] arXiv:2205.08786 (crosslist from cs.PL) [pdf, other]

Title: Fair Termination of Multiparty SessionsSubjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)
There exists a broad family of multiparty sessions in which the progress of one session participant is not unconditional, but depends on the choices performed by other participants. These sessions fall outside the scope of currently available session type systems that guarantee progress. In this work we propose the first type system ensuring that welltyped multiparty sessions, including those exhibiting the aforementioned dependencies, fairly terminate. Fair termination is termination under a fairness assumption that disregards those interactions deemed unfair and therefore unrealistic. Fair termination, combined with the usual safety properties ensured within sessions, not only is desirable per se, but it entails progress and enables a compositional form of static analysis such that the welltyped composition of fairly terminating sessions results in a fairly terminating program.
 [14] arXiv:2205.08916 (crosslist from math.CT) [pdf, other]

Title: Monoidal Width: Capturing Rank WidthComments: 28 pagesSubjects: Category Theory (math.CT); Logic in Computer Science (cs.LO)
Monoidal width was recently introduced by the authors as a measure of the complexity of decomposing morphisms in monoidal categories. We have shown that in a monoidal category of cospans of graphs, monoidal width and its variants can be used to capture tree width, path width and branch width. In this paper we study monoidal width in a category of matrices, and in an extension to a different monoidal category of open graphs, where the connectivity information is handled with matrix algebra and graphs are composed along edges instead of vertices. We show that here monoidal width captures rank width: a measure of graph complexity that has received much attention in recent years.
 [15] arXiv:2205.09027 (crosslist from quantph) [pdf, other]

Title: Coend Optics for Quantum CombsSubjects: Quantum Physics (quantph); Logic in Computer Science (cs.LO); Category Theory (math.CT)
We compare two possible ways of defining a category of 1combs, the first intensionally as coend optics and the second extensionally as a quotient by the operational behaviour of 1combs on lowerorder maps. We show that there is a full and bijective on objects functor quotienting the intensional definition to the extensional one and give some sufficient conditions for this functor to be an isomorphism of categories. We also show how the constructions for 1combs can be extended to produce polycategories of ncombs with similar results about when these polycategories are equivalent. The extensional definition is of particular interest in the study of quantum combs and we hope this work might produce further interest in the usage of optics for modelling these structures in quantum theory.
[ showing up to 2000 entries per page: fewer  more ]
Disable MathJax (What is MathJax?)
Links to: arXiv, form interface, find, cs, recent, 2205, contact, help (Access key information)