We address a fundamental question concerning spatio-temporal database systems: “What are exactly spatio-temporal queries” We define spatio-temporal queries to be computable mappings that are also generic, meaning that the result of a query may only depend to a limited extent on the actual internal representation of the spatio-temporal data. Genericity is defined as invariance under groups of geometric transformations that preserve certain characteristics of spatio-temporal data (e.g., collinearity, distance, velocity, acceleration, …). These groups depend on the notions that are relevant in particular spatio-temporal database applications. These transformations also have the distinctive property that they respect the monotone and unidirectional nature of time.
The degree sequence of an n-vertex graph is d0,…,dn−1, where each di is the number of vertices of degree i in the graph. A random graph with degree sequence d0,…,dn−1 is a randomly selected member of the set of graphs on 1,…,n with that degree sequence, all choices being equally likely. Let λ0,λ1,… be a sequence of nonnegative reals summing to 1. A class of finite graphs has degree sequences approximated by λ0,λ1,… if, for every i and n, the members of the class of size n have λi n o(n) vertices of degree i. Our main result is a convergence law for random graphs with degree sequences approximated by some sequence λ0,λ1,…. With certain conditions on the sequence λ0,λ1,…, the probability of any first-order sentence on random graphs of size n converges to a limit as n grows.
We define notions of resource-bounded continuity and sequentiality for type-two functionals with total inputs, and prove that in the resource-bounded model there are continuous functionals which cannot be efficiently simulated by sequential functionals. We also show that for some naturally defined classes of continuous functionals an efficient simulation is possible.
We present a redevelopment of the theory of real-valued recursive functions that was introduced by C. Moore in 1996 by analogy with the standard formulation of the integer-valued recursive functions. While his work opened a new line of research on analog computation, the original paper contained some technical inaccuracies. We discuss possible attempts to remove the ambiguity in the behavior of the operators on partial functions, with a focus on his “primitive recursive” functions generated by the differential recursion operator that solves initial value problems. Under a reasonable reformulation, the functions in this class are shown to be analytic and computable in a strong sense in computable analysis. Despite this well-behavedness, the class turns out to be too big to have the originally purported relation to differentially algebraic functions, and hence to C. E. Shannon's model of analog computation.
Formal set theory is traditionally concerned with pure sets; consequently, the satisfiability problem for fragments of set theory was most often addressed (and in many cases positively solved) in the pure framework. In practical applications, however, it is common to assume the existence of a number of primitive objects (sometimes called atoms) that can be members of sets but behave differently from them. If these entities are assumed to be devoid of members, the standard extensionality axiom must be revised; then decidability results can sometimes be achieved via reduction to the pure case and sometimes can be based on direct goal-driven algorithms. An alternative approach to modeling atoms that allows one to retain the original formulation of extensionality was proposed by Quine: atoms are self-singletons. In this article we adopt this approach in coping with the satisfiability problem: We show the decidability of this problem relativized to ∃∀-sentences, and develop a goal-driven unification algorithm.
: In this paper, we present the Timed Abstract State Machine (TASM) language, which is a language for the specification of embedded real-time systems. In theengineering of embedded real-time systems, the correctness of the system is definedin terms of three aspects - function, time, and resource consumption. The goal of theTASM language and its associated toolset is to provide a basis for specification-basedreal-time system engineering where these three aspects can be specified and analyzed ...
This paper presents a verification technique for dense-time MTL based on discretization. The technique reduces the validity problem of MTL formulas from dense to discrete time, through the notion of sampling invariance, introduced in previous work [13]. Since the reduction is from an undecidable problem to a decidable one, the technique is necessarily incomplete, so it fails to provide conclusive answers for some formulas. The paper discusses this shortcoming and hints at how it can be mitigated in practice. The verification technique has been implemented on top of the ℤot tool [19] for discrete-time bounded validity checking; the paper also reports on in-the-small experiments with the tool, which show some results that are promising in terms of performance.
The paper addresses the problem of agents compatibility and their conformance to protocols. We assume that the specification of protocols is given in an action theory by means of temporal constraints and, in particular, communicative actions are defined in terms of their effects and preconditions on the social state of the protocol. We show that the problem of verifying the conformance of an agent with a protocol can be solved by making use of an automata based approach, and that the conformance of a set of agents with a protocol guarantees that their interaction cannot produce deadlock situations and it only gives rise to runs of the protocol.
We present a tableau-based algorithm for obtaining a Büchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Büchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton. We also extend the construction to the Product Version of DLTL.
We extend the Description Logic with a “typicality” operator T that allows us to reason about the prototypical properties and inheritance with exceptions. The resulting logic is called . The typicality operator is intended to select the “most normal” or “most typical” instances of a concept. In our framework, knowledge bases may then contain, in addition to ordinary ABoxes and TBoxes, subsumption relations of the form “T(C) is subsumed by P”, expressing that typical C-members have the property P. The semantics of a typicality operator is defined by a set of postulates that are strongly related to Kraus-Lehmann-Magidor axioms of preferential logic P. We first show that T enjoys a simple semantics provided by ordinary structures equipped by a preference relation. This allows us to obtain a modal interpretation of the typicality operator. Using such a modal interpretation, we present a tableau calculus for deciding satisfiability of knowledge bases. Our calculus gives a nondeterministic-exponential time decision procedure for satisfiability of . We then extend knowledge bases by a nonmonotonic completion that allows inferring defeasible properties of specific concept instances.
In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also show that these calculi can be the base for uniform proof systems. Moreover, we present CondLean, a theorem prover in Prolog for these calculi.
We present tableau calculi for some logics of nonmonotonic reason ing, as defined by Kraus, Lehmann and Magidor. We give a tableau proofprocedure for all KLM logics, namely preferential, loop-cumulative, cumulative and rational logics. Our calculi are obtained by introducing suitablemodalities to interpret conditional assertions. We provide a decision procedure for the logics considered, and we study their complexity.
Abstract We prove the canonical models introduced in [D] do not exist for some graded normal logics with symmetric models, namelyKB°, KBD°, KBT°, so that we define a new kind of canonical models, the general ones, and show they exist and work well in every case.
In this paper we discuss a uniform method for constructing free modal and distributive modal algebras. This method draws on works by (Abramsky 2005) and (Ghilardi 1995). We revisit the theory of normal forms for modal logic and derive a normal form representation for positive modal logic. We also show that every finitely generated free modal and distributive modal algebra axiomatised by equations of rank 1 is a reduct of a temporal algebra.
