Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTwo-Variable Logic with Two Order Relations
159
0
0.0
(
0
)
Added by
Thomas Schwentick
Publication date
2011
fields
Informatics Engineering
and research's language is
English
Authors
Thomas Schwentick
Ask ChatGPT about the research
No Arabic abstract
It is shown that the finite satisfiability problem for two-variable logic over structures with one total preorder relation, its induced successor relation, one linear order relation and some further unary relations is EXPSPACE-complete. Actually, EXPSPACE-completeness already holds for structures that do not include the induced successor relation. As a special case, the EXPSPACE upper bound applies to two-variable logic over structures with two linear orders. A further consequence is that satisfiability of two-variable logic over data words with a linear order on positions and a linear order and successor relation on the data is decidable in EXPSPACE. As a complementing result, it is shown that over structures with two total preorder relations as well as over structures with one total preorder and two linear order relations, the finite satisfiability problem for two-variable logic is undecidable.
rate research
Read More
Term modal logics (TML) are modal logics with unboundedly many modalities, with quantification over modal indices, so that we can have formulas of the form $exists y. forall x. (Box_x P(x,y) supsetDiamond_y P(y,x))$. Like First order modal logic, TML is also notoriously undecidable, in the sense that even very simple fragments are undecidable. In this paper, we show the decidability of one interesting fragment, that of two variable TML. This is in contrast to two-variable First order modal logic, which is undecidable.
Given a connected graph $G$ and its vertex $x$, let $U_x(G)$ denote the universal cover of $G$ obtained by unfolding $G$ into a tree starting from $x$. Let $T=T(n)$ be the minimum number such that, for graphs $G$ and $H$ with at most $n$ vertices each, the isomorphism of $U_x(G)$ and $U_y(H)$ surely follows from the isomorphism of these rooted trees truncated at depth $T$. Motivated by applications in theory of distributed computing, Norris [Discrete Appl. Math. 1995] asks if $T(n)le n$. We answer this question in the negative by establishing that $T(n)=(2-o(1))n$. Our solution uses basic tools of finite model theory such as a bisimulation version of the Immerman-Lander 2-pebble counting game. The graphs $G_n$ and $H_n$ we construct to prove the lower bound for $T(n)$ also show some other tight lower bounds. Both having $n$ vertices, $G_n$ and $H_n$ can be distinguished in 2-variable counting logic only with quantifier depth $(1-o(1))n$. It follows that color refinement, the classical procedure used in isomorphism testing and other areas for computing the coarsest equitable partition of a graph, needs $(1-o(1))n$ rounds to achieve color stabilization on each of $G_n$ and $H_n$. Somewhat surprisingly, this number of rounds is not enough for color stabilization on the disjoint union of $G_n$ and $H_n$, where $(2-o(1))n$ rounds are needed.
We consider Hoare-style verification for the graph programming language GP 2. In previous work, graph properties were specified by so-called E-conditions which extend nested graph conditions. However, this type of assertions is not easy to comprehend by programmers that are used to formal specifications in standard first-order logic. In this paper, we present an approach to verify GP 2 programs with a standard first-order logic. We show how to construct a strongest liberal postcondition with respect to a rule schema and a precondition. We then extend this construction to obtain strongest liberal postconditions for arbitrary loop-free programs. Compared with previous work, this allows to reason about a vastly generalised class of graph programs. In particular, many programs with nested loops can be verified with the new calculus.
Let S be a commutative semiring. M. Droste and P. Gastin have introduced in 2005 weighted monadic second order logic WMSOL with weights in S. They use a syntactic fragment RMSOL of WMSOL to characterize word functions (power series) recognizable by weighted automata, where the semantics of quantifiers is used both as arithmetical operations and, in the boolean case, as quantification. Already in 2001, B. Courcelle, J.Makowsky and U. Rotics have introduced a formalism for graph parameters definable in Monadic Second order Logic, here called MSOLEVAL with values in a ring R. Their framework can be easily adapted to semirings S. This formalism clearly separates the logical part from the arithmetical part and also applies to word functions. In this paper we give two proofs that RMSOL and MSOLEVAL with values in S have the same expressive power over words. One proof shows directly that MSOLEVAL captures the functions recognizable by weighted automata. The other proof shows how to translate the formalisms from one into the other.
Existing work on theorem proving for the assertion language of separation logic (SL) either focuses on abstract semantics which are not readily available in most applications of program verification, or on concrete models for which completeness is not possible. An important element in concrete SL is the points-to predicate which denotes a singleton heap. SL with the points-to predicate has been shown to be non-recursively enumerable. In this paper, we develop a first-order SL, called FOASL, with an abstracted version of the points-to predicate. We prove that FOASL is sound and complete with respect to an abstract semantics, of which the standard SL semantics is an instance. We also show that some reasoning principles involving the points-to predicate can be approximated as FOASL theories, thus allowing our logic to be used for reasoning about concrete program verification problems. We give some example theories that are sound with respect to different variants of separation logics from the literature, including those that are incompatible with Reynoldss semantics. In the experiment we demonstrate our FOASL based theorem prover which is able to handle a large fragment of separation logic with heap semantics as well as non-standard semantics.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
