Author name cluster

Witold Charatonik

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

11 papers

2 author rows

LPAR Conference 2018 Conference Paper

Two-variable First-Order Logic with Counting in Forests

Witold Charatonik
Yegor Guskov
Ian Pratt-Hartmann
Piotr Witkowski 0001

We consider an extension of two-variable, first-order logic with counting quantifiers and arbitrarily many unary and binary predicates, in which one distinguished predicate is interpreted as the mother-daughter relation in an unranked forest. We show that both the finite satisfiability and the general satisfiability problems for the extended logic are decidable in NExpTime. We also show that the decision procedure for finite satisfiability can be extended to the logic where two distinguished predicates are interpreted as the mother-daughter relations in two independent forests.

Details

CSL Conference 2017 Conference Paper

Extending Two-Variable Logic on Trees

Bartosz Bednarczyk
Witold Charatonik
Emanuel Kieronski

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.

Details

CSL Conference 2015 Conference Paper

Two-variable Logic with Counting and a Linear Order

Witold Charatonik
Piotr Witkowski 0001

We study the finite satisfiability problem for the two-variable fragment of the first-order logic extended with counting quantifiers (C2) and interpreted over linearly ordered structures. We show that the problem is undecidable in the case of two linear orders (in presence of two other binary symbols). In the case of one linear order it is NEXPTIME-complete, even in presence of the successor relation. Surprisingly, the complexity of the problem explodes when we add one binary symbol more: C2 with one linear order and its successor, in presence of other binary predicate symbols, is decidable, but it is as expressive (and as complex) as Vector Addition Systems.

Details

CSL Conference 2008 Conference Paper

Quantified Positive Temporal Constraints

Witold Charatonik
Michal Wrona

Abstract A positive temporal template (or a positive temporal constraint language) is a relational structure whose relations can be defined over countable dense linear order without endpoints using a relational symbol ≤, logical conjunction and disjunction. This paper gives a complete complexity characterization for quantified constraint satisfaction problems (QCSP) over positive temporal languages. Although the constraint satisfaction problem (CSP) for an arbitrary positive temporal language is trivial (all these templates are closed under constant functions), the corresponding QCSP problems are decidable in LOGSPACE or complete for one of the following classes: NLOGSPACE, P, NP or PSPACE.

Details

LPAR Conference 2008 Conference Paper

Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates

Witold Charatonik
Michal Wrona

Abstract A positive temporal template (or a positive temporal constraint language) is a relational structure whose relations can be defined over a dense linear order of rational numbers using a relational symbol ≤, logical conjunction and disjunction. We provide a complexity characterization for quantified constraint satisfaction problems ( QCSP ) over positive temporal languages. The considered QCSP problems are decidable in LOGSPACE or complete for one of the following classes: NLOGSPACE, P, NP, PSPACE. Our classification is based on so-called algebraic approach to constraint satisfaction problems: we first classify positive temporal languages depending on their surjective polymorphisms and then give the complexity of QCSP for each obtained class. The complete characterization is quite complex and does not fit into one paper. Here we prove that QCSP for positive temporal languages is either NP-hard or belongs to P and we give the whole description of the latter case, that is, we show for which positive temporal languages the problem QCSP is in LOGSPACE, and for which it is NLOGSPACE-complete or P-complete. The classification of NP-hard cases is given in a separate paper.

Details

CSL Conference 2005 Conference Paper

Bounded Model Checking of Pointer Programs

Witold Charatonik
Lilia Georgieva
Patrick Maier 0001

Abstract We propose a bounded model checking procedure for programs manipulating dynamically allocated pointer structures. Our procedure checks whether a program execution of length n ends in an error (e. g. a NULL dereference) by testing if the weakest precondition of the error condition together with the initial condition of the program (e. g. program variable x points to a circular list) is satisfiable. We express error conditions as formulas in the 2-variable fragment of the Bernays-Schönfinkel class with equality. We show that this fragment is closed under computing weakest preconditions. We express the initial conditions by unary relations which are defined by monadic Datalog programs. Our main contribution is a small model theorem for the 2-variable fragment of the Bernays-Schönfinkel class extended with least fixed points expressible by certain monadic Datalog programs. The decidability of this extension of first-order logic gives us a bounded model checking procedure for programs manipulating dynamically allocated pointer structures. In contrast to SAT-based bounded model checking, we do not bound the size of the heap a priori, but allow for pointer structures of arbitrary size. Thus, we are doing bounded model checking of infinite state transition systems.

Details

TCS Journal 2003 Journal Article

Model checking mobile ambients

Witold Charatonik
Silvano Dal Zilio
Andrew D. Gordon
Supratik Mukhopadhyay
Jean-Marc Talbot

We settle the complexity bounds of the model checking problem for the ambient calculus with public names against the ambient logic. We show that if either the calculus contains replication or the logic contains the guarantee operator, the problem is undecidable. In the case of the replication-free calculus and guarantee-free logic we prove that the problem is PSPACE-complete. For the complexity upper bound, we devise a new representation of processes that remains of polynomial size during process execution; this allows us to keep the model checking procedure in polynomial space. Moreover, we prove PSPACE-hardness of the problem for several quite simple fragments of the calculus and the logic; this suggests that there are no interesting fragments with polynomial-time model checking algorithms.

Details DOI

I&C Journal 2002 Journal Article

Set Constraints with Intersection

Witold Charatonik
Andreas Podelski

Set constraints are inclusions between expressions denoting sets of trees. The efficiency of their satisfiability test is a central issue in set-based program analysis, their main application domain. We introduce the class of set constraints with intersection (the only operators forming the expressions are constructors and intersection) and show that its satisfiability problem is DEXPTIME-complete. The complexity characterization continues to hold for negative set constraints with intersection (which have positive and negated inclusions). We reduce the satisfiability problem for these constraints to one over the interpretation domain of nonempty sets of trees. Set constraints with intersection over the domain of nonempty sets of trees enjoy the fundamental property of independence of negated conjuncts. This allows us to handle each negated inclusion separately by the entailment algorithm that we devise. We furthermore prove that set constraints with intersection are equivalent to the class of definite set constraints and thereby settle the complexity question of the historically first class for which the decidability question was solved.

Details DOI

CSL Conference 2001 Conference Paper

The Decidability of Model Checking Mobile Ambients

Witold Charatonik
Jean-Marc Talbot

Abstract The ambient calculus is a formalism for describing the mobility of both software and hardware. The ambient logic is a modal logic designed to specify properties of distributed and mobile computations programmed in the ambient calculus. In this paper we investigate the border between decidable and undecidable cases of model checking mobile ambients for some fragments of the ambient calculus and the ambient logic. Recently, Cardelli and Gordon presented a model-checking algorithm for a fragment of the calculus (without name restriction and without replication) against a fragment of the logic (without composition adjunct) and asked the question, whether this algorithm could be extended to include either replication in the calculus or composition adjunct in the logic. Here we answer this question negatively: it is not possible to extend the algorithm, because each of these extensions leads to undecidability of the problem. On the other hand, we extend the algorithm to the calculus with name restriction and logic with new constructs for reasoning about restricted names.

Details

I&C Journal 1998 Journal Article

Set Constraints in Some Equational Theories

Witold Charatonik

Set constraints are relations between sets of ground terms over a given alphabet. They give a natural formalism for many problems in program analysis, type inference, order-sorted unification, and constraint logic programming. In this paper we start studies of set constraints in the environment given by equational specifications. We show that in the case of associativity (i. e. , in free monoids) as well as in the case of associativity and commutativity (i. e. , in commutative monoids) the problem of consistency of systems of set constraints is undecidable; in linear nonerasing shallow theories the consistency of systems of positive set constraints is NEXPTIME-complete and in linear shallow theories the problem for positive and negative set constraints is decidable.

Details DOI

FOCS Conference 1994 Conference Paper

Set constraints with projections are in NEXPTIME

Witold Charatonik
Leszek Pacholski

Systems of set constraints describe relations between sets of ground terms. They have been successfully used in program analysis and type inference. In this paper we prove that the problem of existence of a solution of a system of set constraints with projections is in NEXPTIME, and thus that it is NEXPTIME-complete. This extends the result of A. Aiken, D. Kozen, and E. L. Wimmers (1993) and R. Gilleron, S. Tison, and M. Tommasi (1990) on decidability of negated set constraints and solves a problem that was open for several years. >

Details