-
Pebble-Intervals Automata and FO2 with Two Orders (Extended Version)
Authors:
Nadia Labai,
Tomer Kotek,
Magdalena Ortiz,
Helmut Veith
Abstract:
We introduce a novel automata model, called pebble-intervals automata (PIA), and study its power and closure properties. PIAs are tailored for a decidable fragment of FO that is important for reasoning about structures that use data values from infinite domains: the two-variable fragment with one total preorder and its induced successor relation, one linear order, and an arbitrary number of unary…
▽ More
We introduce a novel automata model, called pebble-intervals automata (PIA), and study its power and closure properties. PIAs are tailored for a decidable fragment of FO that is important for reasoning about structures that use data values from infinite domains: the two-variable fragment with one total preorder and its induced successor relation, one linear order, and an arbitrary number of unary relations. We prove that the string projection of every language of data words definable in the logic is accepted by a pebble-intervals automaton A, and obtain as a corollary an automata-theoretic proof of the EXPSPACE upper bound for finite satisfiability due to Schwentick and Zeume.
△ Less
Submitted 3 December, 2019; v1 submitted 30 November, 2019;
originally announced December 2019.
-
The exact complexity of the Tutte polynomial
Authors:
Tomer Kotek,
Johann A. Makowsky
Abstract:
This is a survey on the exact complexity of computing the Tutte polynomial. It is the longer 2017 version of Chapter 25 of the CRC Handbook on the Tutte polynomial and related topics, edited by J. Ellis-Monaghan and I. Moffatt, which is due to appear in the first quarter of 2020. In the version to be published in the Handbook the Sections 5 and 6 are shortened and made into a single section.
This is a survey on the exact complexity of computing the Tutte polynomial. It is the longer 2017 version of Chapter 25 of the CRC Handbook on the Tutte polynomial and related topics, edited by J. Ellis-Monaghan and I. Moffatt, which is due to appear in the first quarter of 2020. In the version to be published in the Handbook the Sections 5 and 6 are shortened and made into a single section.
△ Less
Submitted 20 October, 2019;
originally announced October 2019.
-
On the complexity of generalized chromatic polynomials
Authors:
A. Goodall,
M. Hermann,
T. Kotek,
J. A. Makowsky,
S. D. Noble
Abstract:
J. Makowsky and B. Zilber (2004) showed that many variations of graph colorings, called CP-colorings in the sequel, give rise to graph polynomials. This is true in particular for harmonious colorings, convex colorings, mcc_t-colorings, and rainbow colorings, and many more. N. Linial (1986) showed that the chromatic polynomial $χ(G;X)$ is #P-hard to evaluate for all but three values X=0,1,2, where…
▽ More
J. Makowsky and B. Zilber (2004) showed that many variations of graph colorings, called CP-colorings in the sequel, give rise to graph polynomials. This is true in particular for harmonious colorings, convex colorings, mcc_t-colorings, and rainbow colorings, and many more. N. Linial (1986) showed that the chromatic polynomial $χ(G;X)$ is #P-hard to evaluate for all but three values X=0,1,2, where evaluation is in P. This dichotomy includes evaluation at real or complex values, and has the further property that the set of points for which evaluation is in P is finite. We investigate how the complexity of evaluating univariate graph polynomials that arise from CP-colorings varies for different evaluation points. We show that for some CP-colorings (harmonious, convex) the complexity of evaluation follows a similar pattern to the chromatic polynomial. However, in other cases (proper edge colorings, mcc_t-colorings, H-free colorings) we could only obtain a dichotomy for evaluations at non-negative integer points. We also discuss some CP-colorings where we only have very partial results.
△ Less
Submitted 23 January, 2017;
originally announced January 2017.
-
On the automated verification of web applications with embedded SQL
Authors:
Shachar Itzhaky,
Tomer Kotek,
Noam Rinetzky,
Mooly Sagiv,
Orr Tamir,
Helmut Veith,
Florian Zuleger
Abstract:
A large number of web applications is based on a relational database together with a program, typically a script, that enables the user to interact with the database through embedded SQL queries and commands. In this paper, we introduce a method for formal automated verification of such systems which connects database theory to mainstream program analysis. We identify a fragment of SQL which captu…
▽ More
A large number of web applications is based on a relational database together with a program, typically a script, that enables the user to interact with the database through embedded SQL queries and commands. In this paper, we introduce a method for formal automated verification of such systems which connects database theory to mainstream program analysis. We identify a fragment of SQL which captures the behavior of the queries in our case studies, is algorithmically decidable, and facilitates the construction of weakest preconditions. Thus, we can integrate the analysis of SQL queries into a program analysis tool chain. To this end, we implement a new decision procedure for the SQL fragment that we introduce. We demonstrate practical applicability of our results with three case studies, a web administrator, a simple firewall, and a conference management system.
△ Less
Submitted 6 October, 2016;
originally announced October 2016.
-
Monadic second order finite satisfiability and unbounded tree-width
Authors:
Tomer Kotek,
Helmut Veith,
Florian Zuleger
Abstract:
The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese (1991). We prove the following problem is decidable:
Input: (i) A monadic second order logic sentence $α$, and (ii) a sentence $β$ in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of…
▽ More
The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese (1991). We prove the following problem is decidable:
Input: (i) A monadic second order logic sentence $α$, and (ii) a sentence $β$ in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of $α$ and $β$ may intersect.
Output: Is there a finite structure which satisfies $α\landβ$ such that the restriction of the structure to the vocabulary of $α$ has bounded tree-width? (The tree-width of the desired structure is not bounded.)
As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic extending monadic second order logic with linear cardinality constraints of the form $|X_{1}|+\cdots+|X_{r}|<|Y_{1}|+\cdots+|Y_{s}|$, where the $X_{i}$ and $Y_{j}$ are monadic second order variables. We prove the decidability of a similar extension of WS1S.
△ Less
Submitted 16 April, 2016; v1 submitted 25 May, 2015;
originally announced May 2015.
-
Efficient computation of generalized Ising polynomials on graphs with fixed clique-width
Authors:
Tomer Kotek,
Johann A. Makowsky
Abstract:
Graph polynomials which are definable in Monadic Second Order Logic (MSOL) on the vocabulary of graphs are Fixed-Parameter Tractable (FPT) with respect to clique-width. In contrast, graph polynomials which are definable in MSOL on the vocabulary of hypergraphs are fixed-parameter tractable with respect to tree-width, but not necessarily with respect to clique width. No algorithmic meta-theorem is…
▽ More
Graph polynomials which are definable in Monadic Second Order Logic (MSOL) on the vocabulary of graphs are Fixed-Parameter Tractable (FPT) with respect to clique-width. In contrast, graph polynomials which are definable in MSOL on the vocabulary of hypergraphs are fixed-parameter tractable with respect to tree-width, but not necessarily with respect to clique width. No algorithmic meta-theorem is known for the computation of graph polynomials definable in MSOL on the vocabulary of hypergraphs with respect to clique-width. We define an infinite class of such graph polynomials extending the class of graph polynomials definable in MSOL on the vocabulary of graphs and prove that they are Fixed-Parameter Polynomial Time (FPPT) computable, i.e. that they can be computed in time $O(n^{f(k)})$, where $n$ is the number of vertices and $k$ is the clique-width.
△ Less
Submitted 25 May, 2015;
originally announced May 2015.
-
Extending ALCQIO with reachability
Authors:
Tomer Kotek,
Mantas Simkus,
Helmut Veith,
Florian Zuleger
Abstract:
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 A…
▽ More
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 compositions such as list of trees.
We show that the finite satisfiability and implication problems of ALCQIO_{b,Re}-formulae are polynomial-time reducible to finite satisfiability of ALCQIO-formulae. As a consequence, we get that finite satisfiability and finite implication in ALCQIO_{b,Re} are NEXPTIME-complete. Description logics with transitive closure constructors have been studied before, but ALCQIO_{b,Re} is the first description logic that remains decidable on finite structures while allowing at the same time nominals, inverse roles, counting quantifiers and reachability assertions,
△ Less
Submitted 9 July, 2014; v1 submitted 27 February, 2014;
originally announced February 2014.
-
Shape and Content: Incorporating Domain Knowledge into Shape Analysis
Authors:
Diego Calvanese,
Tomer Kotek,
Mantas Šimkus,
Helmut Veith,
Florian Zuleger
Abstract:
The verification community has studied dynamic data structures primarily in a bottom-up way by analyzing pointers and the shapes induced by them. Recent work in fields such as separation logic has made significant progress in extracting shapes from program source code. Many real world programs however manipulate complex data whose structure and content is most naturally described by formalisms fro…
▽ More
The verification community has studied dynamic data structures primarily in a bottom-up way by analyzing pointers and the shapes induced by them. Recent work in fields such as separation logic has made significant progress in extracting shapes from program source code. Many real world programs however manipulate complex data whose structure and content is most naturally described by formalisms from object oriented programming and databases. In this paper, we look at the verification of programs with dynamic data structures from the perspective of content representation. Our approach is based on description logic, a widely used knowledge representation paradigm which gives a logical underpinning for diverse modeling frameworks such as UML and ER. Technically, we assume that we have separation logic shape invariants obtained from a shape analysis tool, and requirements on the program data in terms of description logic. We show that the two-variable fragment of first order logic with counting and trees %(whose decidability was proved at LICS 2013) can be used as a joint framework to embed suitable fragments of description logic and separation logic.
△ Less
Submitted 9 July, 2014; v1 submitted 23 December, 2013;
originally announced December 2013.
-
Connection Matrices and the Definability of Graph Parameters
Authors:
Tomer Kotek,
Johann A. Makowsky
Abstract:
In this paper we extend and prove in detail the Finite Rank Theorem for connection matrices of graph parameters definable in Monadic Second Order Logic with counting (CMSOL) from B. Godlin, T. Kotek and J.A. Makowsky (2008) and J.A. Makowsky (2009). We demonstrate its vast applicability in simplifying known and new non-definability results of graph properties and finding new non-definability resu…
▽ More
In this paper we extend and prove in detail the Finite Rank Theorem for connection matrices of graph parameters definable in Monadic Second Order Logic with counting (CMSOL) from B. Godlin, T. Kotek and J.A. Makowsky (2008) and J.A. Makowsky (2009). We demonstrate its vast applicability in simplifying known and new non-definability results of graph properties and finding new non-definability results for graph parameters. We also prove a Feferman-Vaught Theorem for the logic CFOL, First Order Logic with the modular counting quantifiers.
△ Less
Submitted 27 October, 2014; v1 submitted 16 August, 2013;
originally announced August 2013.
-
Complexity of Ising Polynomials
Authors:
Tomer Kotek
Abstract:
This paper deals with the partition function of the Ising model from statistical mechanics, which is used to study phase transitions in physical systems. A special case of interest is that of the Ising model with constant energies and external field. One may consider such an Ising system as a simple graph together with vertex and edge weights. When these weights are considered indeterminates, the…
▽ More
This paper deals with the partition function of the Ising model from statistical mechanics, which is used to study phase transitions in physical systems. A special case of interest is that of the Ising model with constant energies and external field. One may consider such an Ising system as a simple graph together with vertex and edge weights. When these weights are considered indeterminates, the partition function for the constant case is a trivariate polynomial Z(G;x,y,z). This polynomial was studied with respect to its approximability by L. A. Goldberg, M. Jerrum and M. Paterson in 2003. Z(G;x,y,z) generalizes a bivariate polynomial Z(G;t,y), which was studied by D. Andrén and K. Markström in 2009.
We consider the complexity of Z(G;t,y) and Z(G;x,y,z) in comparison to that of the Tutte polynomial, which is well-known to be closely related to the Potts model in the absence of an external field. We show that Z(G;\x,\y,\z) is #P-hard to evaluate at all points in $mathbb{Q}^3$, except those in an exception set of low dimension, even when restricted to simple graphs which are bipartite and planar. A counting version of the Exponential Time Hypothesis, #ETH, was introduced by H. Dell, T. Husfeldt and M. Wahlén in 2010 in order to study the complexity of the Tutte polynomial. In analogy to their results, we give a dichotomy theorem stating that evaluations of Z(G;t,y) either take exponential time in the number of vertices of $G$ to compute, or can be done in polynomial time. Finally, we give an algorithm for computing Z(G;x,y,z) in polynomial time on graphs of bounded clique-width, which is not known in the case of the Tutte polynomial.
△ Less
Submitted 13 June, 2012; v1 submitted 17 October, 2011;
originally announced October 2011.
