Search results for "decidability"
showing 10 items of 46 documents
Probabilistic and team PFIN-type learning: General properties
2008
We consider the probability hierarchy for Popperian FINite learning and study the general properties of this hierarchy. We prove that the probability hierarchy is decidable, i.e. there exists an algorithm that receives p_1 and p_2 and answers whether PFIN-type learning with the probability of success p_1 is equivalent to PFIN-type learning with the probability of success p_2. To prove our result, we analyze the topological structure of the probability hierarchy. We prove that it is well-ordered in descending ordering and order-equivalent to ordinal epsilon_0. This shows that the structure of the hierarchy is very complicated. Using similar methods, we also prove that, for PFIN-type learning…
The Fluted Fragment with Transitivity
2019
We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.
Finite automata on timed ω-trees
2003
AbstractIn the last decade Alur and Dill introduced a model of automata on timed ω-sequences which extends the traditional models of finite automata. In this paper, we present a theory of timed ω-trees which extends both the theory of timed ω-sequences and the theory of ω-trees. The main motivation is to introduce a new way of specifying real-time systems and provide tools for studying decidability problems in related fields. We focus on the decision problems and their applications in system verification and synthesis.
RECOGNIZABLE PICTURE LANGUAGES
1992
The purpose of this paper is to propose a new notion of recognizability for picture (two-dimensional) languages extending the characterization of one-dimensional recognizable languages in terms of local languages and alphabetic mappings. We first introduce the family of local picture languages (denoted by LOC) and, in particular, prove the undecidability of the emptiness problem. Then we define the new family of recognizable picture languages (denoted by REC). We study some combinatorial and language theoretic properties of REC such as ambiguity, closure properties or undecidability results. Finally we compare the family REC with the classical families of languages recognized by four-way a…
Decidability Frontier for Fragments of First-Order Logic with Transitivity
2018
Several decidable fragments of first-order logic have been identified in the past as a generalisation of the standard translation of modal logic. These include: the fluted fragment, the two-variable frag- ment, the guarded fragment and the unary negation fragment; some of them have been recently generalised or combined to yield even more expressive decidable logics (guarded negation fragment or uniform one- dimensional fragment). None of the fragments allows one to express tran- sitivity of a binary relation or related properties like being an equivalence, a linear or a partial order, that naturally appear in specifications or in verification. The question therefore arises what is the impac…
The fluted fragment revisited
2019
AbstractWe study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, motivated by the work of W. V. Quine. We show that the satisfiability problem for this fragment has nonelementary complexity, thus refuting an earlier published claim by W. C. Purdy that it is in NExpTime. More precisely, we consider ${\cal F}{{\cal L}^m}$, the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all $m \ge 1$. We show that, for $m \ge 2$, this subfragment forces $\left\lfloor {m/2} \right\rfloor$-tuply exponentially large models, and that its satisfiability problem is $\left\lfloor {m/2} \right\rfloor$-NExpTime-hard. We…
The guarded fragment with transitive guards
2004
The guarded fragment with transitive guards, (GF+TG), is an extension of the guarded frag- ment of 9rst-order logic, GF, in which certain predicates are required to be transitive, transitive predicate letters appear only in guards of the quanti9ers and the equality symbol may appear everywhere. We prove that the decision problem for (GF+TG) is decidable. Moreover, we show that the problem is in 2EXPTIME. This result is optimal since the satis9ability problem for GF is 2EXPTIME-complete (J. Symbolic Logic 64 (1999) 1719-1742). We also show that the satis- 9ability problem for two-variable (GF+TG) is NEXPTIME-hard in contrast to GF with bounded number of variables for which the satis9ability …
Feasibility of finite and infinite paths in data dependent programs
2005
This paper considers the feasibility of finite and infinite paths in programs in two simple programming languages. The language LBASE allows to express the dependencies of real time systems on integer data, the language LTIM can model quantitative timing constraints in r.t.s. specifications. It is proven that the problem of whether a given LBASE or LTIM program has an infinite feasible path (i.e. whether it can exhibit an infinite behaviour) is decidable. The possibilities to characterise the sets of all feasible finite and infinite paths in LBASE and LTIM programs are also discussed. The infinite feasible path existence problem is proven decidable also for the language LTIBA which has both…
Two-variable logics with counting and semantic constraints
2018
In this article we discuss fragments and extensions of two-variable logics motivated by practical applications. We outline the decidability frontier, describing some of the techniques developed for deciding satisfiability and finite satisfiability, as well as characterizing their complexity.
Deciding properties of integral relational automata
1994
This paper investigates automated model checking possibilities for CTL* formulae over infinite transition systems represented by relational automata (RA). The general model checking problem for CTL* formulae over RA is shown undecidable, the undecidability being observed already on the class of Restricted CTL formulae. The decidability result, however, is obtained for another substantial subset of the logic, called A-CTL*+, which includes all ”linear time” formulae.