اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدWeighted Automata and Monadic Second Order Logic
87
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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.
قيم البحث
اقرأ أيضاً
We characterise the sentences in Monadic Second-order Logic (MSO) that are over finite structures equivalent to a Datalog program, in terms of an existential pebble game. We also show that for every class C of finite structures that can be expressed
in MSO and is closed under homomorphisms, and for all integers l,k, there exists a *canonical* Datalog program Pi of width (l,k), that is, a Datalog program of width (l,k) which is sound for C (i.e., Pi only derives the goal predicate on a finite structure A if A is in C) and with the property that Pi derives the goal predicate whenever *some* Datalog program of width (l,k) which is sound for C derives the goal predicate. The same characterisations also hold for Guarded Second-order Logic (GSO), which properly extends MSO. To prove our results, we show that every class C in GSO whose complement is closed under homomorphisms is a finite union of constraint satisfaction problems (CSPs) of countably categorical structures.
We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations o
f the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., each formula that is valid on all finite trees is provable using our axioms. As a backdrop to our positive results, on arbitrary structures, the logics that we study are known to be non-recursively axiomatizable.
Linear temporal logic was introduced in order to reason about reactive systems. It is often considered with respect to infinite words, to specify the behaviour of long-running systems. One can consider more general models for linear time, using words
indexed by arbitrary linear orderings. We investigate the connections between temporal logic and automata on linear orderings, as introduced by Bruy`ere and Carton. We provide a doubly exponential procedure to compute from any LTL formula with Until, Since, and the Stavi connectives an automaton that decides whether that formula holds on the input word. In particular, since the emptiness problem for these automata is decidable, this transformation gives a decision procedure for the satisfiability of the logic.
The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese (1991). We prove the following problem is decidable: Input: (i) A monadic second order l
ogic sentence $alpha$, and (ii) a sentence $beta$ in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of $alpha$ and $beta$ may intersect. Output: Is there a finite structure which satisfies $alphalandbeta$ such that the restriction of the structure to the vocabulary of $alpha$ has bounded tree-width? (The tree-width of the desired structure is not bounded.) As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic extending monadic second order logic with linear cardinality constraints of the form $|X_{1}|+cdots+|X_{r}|<|Y_{1}|+cdots+|Y_{s}|$, where the $X_{i}$ and $Y_{j}$ are monadic second order variables. We prove the decidability of a similar extension of WS1S.
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $bigwedge_{i=1}^n mathbf{G}mathbf{F} varphi_i vee mathb
f{F}mathbf{G} psi_i$, where $varphi_i$ and $psi_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
