Questions tagged [finite-model-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0 votes
0 answers
17 views

Practical applications of finite model theory to databases

I have heard that finite model theory has connections to database theory. Is there an example of where this database theory could be used by programmers developing database applications?
Andrew's user avatar
  • 287
0 votes
0 answers
60 views

How to find the intersection of two FAs and then check if two FAs are equal?

I am still quite confused on how to properly handle in answering the intersection and equality of two FAs in terms of table form and manipulating its transformation....
Ralph Henry's user avatar
1 vote
0 answers
104 views

Horn formulas, existential second order logic and the Cardinality constraint

Consider this Problem $P$ as follows: $~$ Given a set $S$ and a constant $K$.. $~$Is there a subset $M$ of $S$, such that $|M| \ge K$? Of course, $P$ can be easily solved in time polynomial in $|S|$.. ...
Shuxue Jiaoshou's user avatar
3 votes
1 answer
124 views

How to describe Deterministic Transitive Closure in FOL?

In "Finite Model Theory and Its Applications", page 152, it is said that Deterministic Transitive Closure, on ordered finite structures, captures LOGSPACE. Hence, taking into account that ...
441Juggler's user avatar
0 votes
0 answers
23 views

About quasi-linear finite automata

Let M a finite state transducer define as : $M=<X,Y,S,\delta,\lambda>$ What we mean by quasi-linear finite automata?
Hicham ATATRI's user avatar
4 votes
2 answers
82 views

Defining $a^n b^{n^2}$ with one existential SO binary relation

Is it possible to define the language: $$L = \{ a^n \; b^{n^2} \}$$ using an existential second order sentence over strings (ordered structures with unary predicates $U_a(x), U_b(x)$) using only ...
Vor's user avatar
  • 12.4k
1 vote
0 answers
71 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 ...
Troy McClure's user avatar
2 votes
0 answers
66 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 ...
kne's user avatar
  • 2,164
2 votes
1 answer
283 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 ...
Troy McClure's user avatar
2 votes
1 answer
50 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: $...
Jacob Arbib's user avatar
0 votes
2 answers
161 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.
Marco's user avatar
  • 41
-2 votes
1 answer
453 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 ...
imanshu15's user avatar
  • 101
5 votes
2 answers
359 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, ...
aki's user avatar
  • 51
15 votes
0 answers
291 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 ...
Vor's user avatar
  • 12.4k
12 votes
2 answers
3k 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 ...
Ram's user avatar
  • 223
5 votes
2 answers
664 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$ ...
pritam's user avatar
  • 191
4 votes
0 answers
148 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 ...
pritam's user avatar
  • 191
20 votes
3 answers
344 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 ...
Kaveh's user avatar
  • 21.9k
19 votes
2 answers
1k 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 ...
Ken Li's user avatar
  • 3,058