Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [finite-model-theory]

The tag has no usage guidance.

2
votes
0answers
29 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
206 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
22 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
121 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
388 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
161 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
186 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
514 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
608 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 ...