Search

The author has recently introduced an abstract algebraic framework of analogical proportions within the general setting of universal algebra. This paper studies analogical proportions in the boolean domain consisting of two elements 0 and 1 within his framework. It turns out that our notion of boolean proportions coincides with two prominent models from the literature in different settings. This means that we can capture two separate modellings of boolean proportions within a single framework which is mathematically appealing and provides further evidence for the robustness and applicability of the general framework. [ABSTRACT FROM AUTHOR]

Baba is You is a 2019 indie puzzle game whose levels are two-dimensional grids of objects. This paper demonstrates how a universal Turing machine could be created as a custom level in the game if a specific in-game limit were to be removed. A player could perform any computation by playing this level, allowing infinitely many new and meaningful puzzles to be created. Furthermore, the construction is such that the level is won if and only if the Turing machine halts, proving perfect play of the game to be unattainable by any computer. The machine is found to be exponentially time-complex, and the paper concludes with a discussion of the practical feasibility of in-game computation. [ABSTRACT FROM AUTHOR]

We prove that ω-languages of (non-deterministic) Petri nets and ω-languages of (nondeterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of ω-languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of ω-languages of (non-deterministic) Turing machines. We also show that it is highly undecidable to determine the topological complexity of a Petri net ω-language. Moreover, we infer from the proofs of the above results that the equivalence and the inclusion problems for ω-languages of Petri nets are ∏ 2 1 -complete, hence also highly undecidable. Additionally, we show that the situation is quite the opposite when considering unambiguous Petri nets, which have the semantic property that at most one accepting run exists on every input. We provide a procedure of determinising them into deterministic Muller counter machines with counter copying. As a consequence, we entail that the ω-languages recognisable by unambiguous Petri nets are △ 3 0 sets. [ABSTRACT FROM AUTHOR]

We prove that one can construct various kinds of automata over finite words for which some elementary properties are actually independent from strong set theories like T n = : Z F C + "There exist (at least) n inaccessible cardinals", for integers n ≥ 0. In particular, we prove independence results for languages of finite words generated by context-free grammars, or accepted by 2-tape or 1-counter automata. Moreover we get some independence results for weighted automata and for some related finitely generated subsemigroups of the set ℤ 3 × 3 of 3-3 matrices with integer entries. Some of these latter results are independence results from the Peano axiomatic system PA. [ABSTRACT FROM AUTHOR]

The complexity of the model checking problem for various fragments of first-order logic (FO) has attracted much attention over the last two decades, in particular for the fragment induced by E and ^ and that induced by A, E, and ^, which are better known as the constraint satisfaction problem and the quantified constraint satisfaction problem, respectively. The former was conjectured to follow a dichotomy between P and NP-complete by Feder and Vardi [SIAM J. Comput., 28 (1998), pp. 57-104]. For the latter, there are several partial trichotomy results between P, NP-complete, and Pspace-complete, and Chen [Meditations on quantified constraint satisfaction, in Logic and Program Semantics, Springer, Heidelberg, 2012, pp. 35-49] ventured a conjecture regarding Pspace-completeness vs. membership in NP in the presence of constants. We give a comprehensive account of the whole field of the complexity of model checking similar syntactic fragments of FO. The above two fragments are in fact the only ones for which there is currently no known complexity classification. Indeed, we consider all other similar syntactic fragments of FO, induced by the presence or absence of quantifiers and connectives, and fully classify the complexities of the parameterization of the model-checking problem by a finite model D, that is, the expression complexities for certain finite D. Perhaps surprisingly, we show that for most of these fragments, "tractability" is witnessed by a generic solving algorithm which uses quantifier relativization. Our classification methodology relies on tailoring suitably the algebraic approach pioneered by Jeavons, Cohen, and Gyssens [J. ACM, 44 (1997), pp. 527-548] for the constraint satisfaction problem and by Börner et al. [Inform. and Comput., 207 (2009), pp. 923-944] for the quantified constraint satisfaction problem. Most fragments under consideration can be relatively easily classified, either directly or using Schaefer's dichotomy theorems for SAT and QSAT, with the notable exception of the positive equality-free fragment induced by E, A, ^, and V. This outstanding fragment can also be classified and enjoys a tetrachotomy: according to the model, the corresponding model checking problem is either tractable, NP-complete, co-NP-complete, or Pspace-complete. [ABSTRACT FROM AUTHOR]

Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. Free short-circuit logic is the equational logic in which compound statements are evaluated from left to right, while atomic evaluations are not memorised throughout the evaluation, i.e. evaluations of distinct occurrences of an atom in a compound statement may yield different truth values. We provide a simple semantics for free short-circuit logic (SCL) and an independent axiomatisation. Finally, we discuss evaluation strategies, some other SCLs, and side effects. [ABSTRACT FROM AUTHOR]

We prove that the determinacy of Gale–Stewart games whose winning sets are infinitary rational relations accepted by 2-tape Büchi automata is equivalent to the determinacy of (effective) analytic Gale–Stewart games which is known to be a large cardinal assumption. Then we prove that winning strategies, when they exist, can be very complex, i.e. highly non-effective, in these games. We prove the same results for Gale–Stewart games with winning sets accepted by real-time 1-counter Büchi automata, then extending previous results obtained about these games. 1. There exists a 2-tape Büchi automaton (respectively, a real-time 1-counter Büchi automaton) A such that: (a) there is a model of ZFC in which Player 1 has a winning strategy σ in the game G ( L ( A ) ) but σ cannot be recursive and not even in the class ( Σ 2 1 ∪ Π 2 1 ) ; (b) there is a model of ZFC in which the game G ( L ( A ) ) is not determined. 2. There exists a 2-tape Büchi automaton (respectively, a real-time 1-counter Büchi automaton) A such that L ( A ) is an arithmetical Δ 3 0 -set and Player 2 has a winning strategy in the game G ( L ( A ) ) but has no hyperarithmetical winning strategies in this game. 3. There exists a recursive sequence of 2-tape Büchi automata (respectively, of real-time 1-counter Büchi automata) A n , n ≥ 1 , such that all games G ( L ( A n ) ) are determined, but for which it is Π 2 1 -complete hence highly undecidable to determine whether Player 1 has a winning strategy in the game G ( L ( A n ) ) . Then we consider the strengths of determinacy for these games, and we prove the following results. 1. There exists a 2-tape Büchi automaton (respectively, a real-time 1-counter Büchi automaton) A ♯ such that the game G ( A ♯ ) is determined iff the effective analytic determinacy holds. 2. There is a transfinite sequence of 2-tape Büchi automata (respectively, of real-time 1-counter Büchi automata) ( A α ) α < ω 1 CK , indexed by recursive ordinals, such that the games G ( L ( A α ) ) have strictly increasing strengths of determinacy. We also show that the determinacy of Wadge games between two players in charge of infinitary rational relations accepted by 2-tape Büchi automata is equivalent to the (effective) analytic Wadge determinacy and thus also equivalent to the (effective) analytic determinacy. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

Abstract: On finite structures, there is a well-known connection between the expressive power of Datalog, finite variable logics, the existential pebble game, and bounded hypertree duality. We study this connection for infinite structures. This has applications for constraint satisfaction with infinite templates. If the template Γ is ω-categorical, we present various equivalent characterizations of those Γ such that the constraint satisfaction problem (CSP) for Γ can be solved by a Datalog program. We also show that can be solved in polynomial time for arbitrary ω-categorical structures Γ if the input is restricted to instances of bounded treewidth. Finally, we characterize those ω-categorical templates whose CSP has Datalog width 1, and those whose CSP has strict Datalog width k. [Copyright &y& Elsevier]

Ordinary Kripke models are not reactive. When we evaluate (test/ measure) a formula A at a model m, the model does not react, respond or change while we evaluate. The model is static and unchanged. This paper studies Kripke models which react to the evaluation process and change themselves during the process. The additional device we add to Kripke semantics to make it reactive is to allow the accessibility relation to access itself. Thus the accessibility relation ${\cal R}$ of a reactive Kripke model contains not only pairs $(a, b) \in {\cal R}$ of possible worlds ( b is accessible to a, i.e., there is an accessibility arc from a to b) but also pairs of the form $(t, (a, b))\in {\cal R}$, meaning that the arc ( a, b) is accessible to t, or even connections of the form $((a,b), (c,d))\in {\cal R}$. This new kind of Kripke semantics allows us to characterise more axiomatic modal logics (with one modality $\square$) by a class of reactive frames. There are logics which cannot be characterised by ordinary frames but which can be characterised by reactive frames. We also discuss the manifestation of the 'reactive' idea in the context of automata theory, where we allow the automaton to react and change it's own definition as it responds to input, and in graph theory, where the graph can change under us as we manipulate it. [ABSTRACT FROM AUTHOR]

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, and the path is s, s,..., s, then the system is ordinary non-reactive system if the options available at s (i.e., which states t we can go to from s) do not depend on the path s,..., s (i.e., do not depend on how we got to s). 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. [ABSTRACT FROM AUTHOR]

Abstract: Hierarchical graph definitions allow a modular description of structures using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions allow us to specify structures of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems when input structures are defined hierarchically. In this paper, the model-checking problem for first-order logic (FO), monadic second-order logic (MSO), and second-order logic (SO) on hierarchically defined input structures is investigated. It is shown that in general these model-checking problems are exponentially harder than their non-hierarchical counterparts, where the input structures are given explicitly. As a consequence, several new complete problems for the levels of the polynomial time hierarchy and the exponential time hierarchy are obtained. Based on classical results of Gaifman and Courcelle, two restrictions on the structure of hierarchical graph definitions that lead to more efficient model-checking algorithms are presented. [Copyright &y& Elsevier]

Abstract: An inferential semantics for full Higher Order Logic (HOL) is proposed. The paper presents a constructive notion of model, that being able to capture relevant computational aspects is particularly suited for the applications of HOL to computer science. The inferential semantics is based on the introduction of new abstract deduction structures (ADS) that express the action of the Comprehension Axiom in a Higher Order Logic proof. The ADS’s allow to define an inferential algebra of higher order potential proof-trees, endowed with two binary operations, the abstraction and the contraction, each consisting of constructive reductions between potential proofs. Typed formulas are interpreted by sequent trees, and the operations between trees correspond to the logical connectives of the interpreted formula. Higher order logic is sound and complete w.r.t. the given inferential semantics. [Copyright &y& Elsevier]

We consider logics which define different properties of functions - such as injectivity, surjectivity, monotonicity, etc. - in the context of temporal×modal logic. In this type of logics, the possible worlds semantics is modified by considering each world as a temporal flow and using accessibility functions to represent the connection among them. This approach is adequate to model interactions between processes with clocks that can be either synchronized or not. We study the definability and give indexed axiomatic systems for these properties. [ABSTRACT FROM AUTHOR]