The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
17th International Workshop CSL 2003, 12th Annual Conference of the EACSL, 8th Kurt Gödel Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003. Proceedings
In an earlier work [AČJYK00] we presented a general framework for verification of infinite-state transition systems, where the transition relation is monotonic with respect to a well quasi-ordering on the set of states. In this paper, we investigate extending the framework from the context of transition systems to that of games. We show that monotonic games are in general undecidable. We identify...
This article discusses the relations between the step-wise development through refinement and the design of test-cases. It turns out that a commuting diagram inspired by the V-process model is able to clarify the issues involved. This V-diagram defines the dependencies of specifications, implementations and test-cases in the category of contracts. The objects in this category are contracts defined...
The functional paradigm of computation has been widely investigated and given a solid mathematical foundation, initiated with the Curry-Howard isomorphism, then elaborated and extended in multiple ways. However, this paradigm is inadequate to capture many useful programming intuitions, arising in particular in the development of applications integrating distributed, autonomous components. Indeed,...
We will speak about three traditions in Logic: – Classical, usually associated with Frege, Hilbert, Gödel, Tarski, and others; – Intuitionistic, founded by Brouwer, Heyting, Kolmogorov, Gödel, Kleene, and others; – Explicit, which we trace back to Skolem, Curry, Gödel, Church, and others. The classical tradition in logic based on quantifiers ∀ and ∃ essentially reflected...
For a fixed countable homogeneous relational structure Γ we study the computational problem whether a given finite structure of the same signature homomorphically maps to Γ. This problem is known as the constraint satisfaction problem CSP(Γ) for Γ and was intensively studied for finite Γ. We show that – as in the case of finite Γ – the computational complexity of CSP(Γ) for countable homogeneous Γ...
The standard constraint satisfaction problem over an arbitrary finite domain can be expressed as follows: given a first-order sentence consisting of a conjunction of predicates, where all of the variables are existentially quantified, determine whether the sentence is true. This problem can be parameterized by the set of allowed constraint predicates. With each predicate, one can associate certain...
The aim of this tutorial is to give an overview on the state-of-the-art in infinite-state model checking and its applications. We present a unified modeling framework based on word/term rewrite systems and show its relevance in reasoning about several important classes of systems (communication protocols, parametrized distributed algorithms, multithreaded programs, etc). Then, we address...
We introduce a fixpoint extension of Hintikka and Sandu’s IF (independence-friendly) logic. We obtain some results on its complexity and expressive power. We relate it to parity games of imperfect information, and show its application to defining independence-friendly modal mu-calculi.
System SKS is a set of rules for classical propositional logic presented in the calculus of structures. Like sequent systems and unlike natural deduction systems, it has an explicit cut rule, which is admissible. In contrast to sequent systems, the cut rule can easily be reduced to atomic form. This allows for a very simple cut elimination procedure based on plugging in parts of a proof, like normalisation...
“Computational mathematics” (algorithmic mathematics) is the part of mathematics that strives at the solution of mathematical problems by algorithms. In a superficial view, some people might believe that computational mathematics is the easy part of mathematics in which trivial mathematics is made useful by repeating trivial steps sufficiently many times on current powerful machines in order to achieve...
Many verification, planning, and control problems can be modeled as games played on state-transition graphs by one or two players whose conflicting goals are to form a path in the graph. The focus here is on simple stochastic parity games, that is, two-player games with turn-based probabilistic transitions and ω-regular objectives formalized as parity (Rabin chain) winning conditions. An efficient...
We give machine characterizations of the complexity classes of the W-hierarchy. Moreover, for every class of this hierarchy, we present a parameterized halting problem complete for this class.
We propose a protocol model which integrates two different ways of analyzing cryptographic protocols: i) analysis w.r.t. an unbounded number of sessions and bounded message size, and ii) analysis w.r.t. an a priori bounded number of sessions but with messages of unbounded size. We show that in this model secrecy is DEXPTIME-complete. This result is obtained by extending the Dolev-Yao intruder to simulate...
We study the proof complexity of Taut, the class of Second-Order Existential (SO∃) logical sentences which fail in all finite models. The Complexity-Gap theorem for Tree-like Resolution says that the shortest Tree-like Resolution refutation of any such sentence Φ is either fully exponential, $2^{\Omega \left(n\right)}$ , or polynomial, $n^{O\left(1\right)}$ , where n is the size of the finite...
The λws-calculus is a λ-calculus with explicit substitutions introduced in [4]. It satisfies the desired properties of such a calculus: step by step simulation of β, confluence on terms with meta-variables and preservation of the strong normalization. It was conjectured in [4] that simply typed terms of λws are strongly normalizable...
Gire and Hoang introduce a fixed-point logic with a ‘symmetric’ choice operator that makes a nondeterministic choice from a definable set of tuples at each stage in the inductive construction of a relation, as long as the set of tuples is an automorphism class of the structure. We present a clean definition of the syntax and semantics of this logic and investigate its expressive power. We extend the...
At CSL 2002, Jerzy Marcinkowsi and Tomasz Truderung presented the notions of positive games and persistent strategies [8]. A strategy is persistent if, given any finite or infinite run played on a game graph, each time the player visits some vertex already encountered, this player repeats the decision made when visiting this vertex for the first time. Such strategies require memory, but once a choice...
Abduction is a fundamental mode of reasoning, which has taken on increasing importance in Artificial Intelligence (AI) and related disciplines. Computing abductive explanations is an important problem, and there is a growing literature on this subject. We contribute to this endeavor by presenting new results on computing multiple resp. all of the possibly exponentially many explanations of an abductive...
In [1,2] Zhang shows how the complexity of cut elimination depends on the nesting of quantifiers in cut formulas. By studying the role of contractions we can refine that analysis and show how the complexity depends on a combination of contractions and quantifier nesting. With the refined analysis the upper bound on cut elimination coincides with Statman’s lower bound. Every non-elementary growth example...
We study the succinctness of monadic second-order logic and a variety of monadic fixed point logics on trees. All these languages are known to have the same expressive power on trees, but some can express the same queries much more succinctly than others. For example, we show that, under some complexity theoretic assumption, monadic second-order logic is non-elementarily more succinct than monadic...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.