Questions tagged [finite-model-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
1
vote
0answers
52 views

Datalog Program Equivalence with Fixed Universe Size

It is well known that to compute equivalence of two Datalog programs (or equivalently of two first order formulas with the least fixed point operator) wrt all possible inputs and universes, is ...
2
votes
0answers
33 views

LTL and alternation

Apparently, model checking LTL on Kripke structures is PSPACE-complete (see this question). Usually, when something in finite model theory is PSPACE-hard, there is a simple proof using the APTIME ...
2
votes
1answer
216 views

Datalog Self Interpretation

According to https://link.springer.com/article/10.1007%2Fs001530050135 (Logics that define their own semantics, Imhof 1999) the logic FO[LFP] can define its own semantics, though the proof (of ...
2
votes
1answer
34 views

How to understand the notion of boolean query via Immerman's definition

A query is any mapping $I:STRUC[\sigma] \to STRUC[\tau]$ that is polynomially bounded. A boolean query is a map $I_b: STRUC[\sigma] \to \{0,1\}$. A boolean query can also be thought as the susbset: $...
0
votes
2answers
123 views

What is meant by the term 'state' in a finite-state machine?

What is meant by the term 'state' in a finite-state machine? I have not seen a proper definition on the web and am looking for a university-level answer. Thank you in advance.
-2
votes
1answer
409 views

Finite State Automaton Transition Diagram

I got an alphabet E={x,y,z}. And i want to create a finite state automaton that accepts strings consisting of at least two x's, followed by at most three y's followed by any number of z's. And i want ...
5
votes
2answers
177 views

propositional Modal logic filtration definition

Hello I have a slightly unusual question which relates to a definition of filtration structure. The following is my current state of the definition: $ \mathcal{M} = (W, R, L) $, W is a set of worlds, ...
14
votes
0answers
193 views

Using logic to prove non-regularity of a language

A language $L$ is regular if and only if it is definiable by a sentence in monadic second order logic (MSO) over strings (J.R. Buchi, Weak second-order arithmetic and Finite automata; Z. Math. Logik ...
11
votes
2answers
2k views

Why is least fixed point (lfp) important in program analysis

I am trying to get a big picture on the importance of least fixed point (lfp) in program analysis. For instance abstract interpretation seems to use the existence of lfp. Many research papers on ...
4
votes
2answers
526 views

Proof of Trakhtenbrot's theorem

In the proof of Trakhtenbrot's theorem (as given in "Elements of Finite Model Theory" by Leonid Libkin), for every Turing machine $M$, author constructs a FO sentence $\Phi_M$ of vocabulary $\sigma$ ...
4
votes
0answers
140 views

Decidability over finite graphs of small degree [closed]

Suppose $\sigma$ is a vocabulary of First Order logic consisting of one binary relation $E$ and let $\phi$ be a $\sigma$ sentence (FO formula with no free variables). Is it decidable whether there is ...
19
votes
3answers
286 views

Extension of SQL capturing $\mathsf{P}$

According to Immerman, the complexity class associated with SQL queries is exactly the class of safe queries in $\mathsf{Q(FO(COUNT))}$ (first-order queries plus counting operator): SQL captures safe ...
18
votes
2answers
640 views

Does the 'difference' operation add expressiveness to a query language that already includes 'join'?

The set difference operator (e.g., EXCEPT in some SQL variants) is one of the many fundamental operators of relational algebra. However, there are some databases ...