2
$\begingroup$

Here's something I've been playing with off and on for a bit; I'm curious if anyone has seen it before.

For this question, a Kripke frame $K$ is a finite reflexive directed graph. (Reflexivity isn't important, but it's convenient.) Given a finite set $P$ of propositional variables, the modal language on $P$ and the set of $P$-valuations on $K$ are what you'd expect: modal sentences are built from $P$ by Booleans and the "$\Box$" operation, a $P$-valuation on $K$ is a map $P\times K\rightarrow \{True, False\}$, and a modal sentence $\varphi$ is true at a world $w\in K$ under a given valuation $V$ if it is true under the usual semantics - $\Box\psi$ is interpreted as "every world seen satisfies $\psi$," and everything else is straightforward.

For details, see http://en.wikipedia.org/wiki/Kripke_semantics.

Now given a Kripke frame $K$, a propositional language $P$, and a valuation $V$, the triple $(K, P, V)$ induces an equivalence relation $\cong_{K, P, V}$ on $K$ given by elementary equivalence: for $u, v\in K$, $u\cong_{K, P, V} v$ if $[(V, u)\models \varphi]\iff[(V, v)\models\varphi]$ for every modal sentence $\varphi$ using propositional letters from $P$.

Okay, now forget the language and valuation: given a Kripke frame $K$, say a partition $\pi$ of $K$ is tame if for some $P$ and $V$ we have $\pi=K/\cong_{K, P, V}$.

For example, clearly the discrete partition of $K$ is always tame, as is the indiscrete partition (this is where we need reflexivity). Moreover, if $\pi_0, \pi_1$ are tame, then their common refinement $\pi_2$ is also tame, so the tame partitions form a lattice.

On the other hand, there are partitions which are not tame: for example, if $K=\langle\{a, b, c\}, \{(a, a), (b, b), (b, c), (c, c)\}\rangle$, then $[\{a, b\}, \{c\}]$ is not a tame partition of $K$ - if we can tell $b$ and $c$ apart then we must be able to tell $a$ and $b$ apart.


There are a bunch of questions I have around tameness of partitions (besides "has anyone seen this?"). Here are the ones I think are most interesting:

  • Is there a snappier description of tameness?

  • When do two Kripke frames with the same vertex set have the same family of tame partitions? (Maybe "same" is not the right notion here . . .)

  • What can we say about the number $\#(K)$ of tame partitions of a frame $K$ (including the complexity of the map $K\mapsto\#(K)$)?

  • If $\mathcal{K}=(K_i)_{i\in\mathbb{N}}$ is a sequence of Kripke frames, let $\#(\mathcal{K})$ be the associated sequence of numbers of tame partitions. What can we say about the behavior of $\#(\mathcal{K})$ for $\mathcal{K}$ a "random" sequence of finite graphs? (Obviously this is vague - the two notions of randomness I'm most interested in are: $K_i$ is picked uniformly randomly from the set of Kripke frames of size $i$; and $K_{i+1}$ is gotten from $K_i$ by adding one new vertex $v$, and then for each old vertex $w$ an edge between $v$ and $w$ with probability $p$.)

$\endgroup$
6
  • $\begingroup$ Why do you assume the graph is directed? Do you mean anti-directed? This would correspond to rooted in a finite transitive rooted frame, which is a common situation with Kripke frames. Usually, I think of (forward) directed transitive reflexive frames as validating S4.2 and complete for S4.2, but your context seems more general than this. Also, you didn't mention bisimilarity or the Jankov-Fine formulas, which seem surely relevant for your context. What do you know about that? $\endgroup$ Commented Mar 12, 2015 at 1:16
  • $\begingroup$ By "directed" I just meant that an edge is an ordered pair $(a, b)$ rather than a set $\{a, b\}$ - that is, edges are arrows, not lines. So, "directed" in the graph theoretic sense. In particular, my underlying logic is $T$, nothing nearly so strong as $S4.2$. As to bisimulation and the Jankov-Fine formulas, I only know very little; anything you can tell me I'm sure would be useful. $\endgroup$ Commented Mar 12, 2015 at 1:21
  • $\begingroup$ Oh, I see, of course you just mean that it is a directed graph; I had mis-read it as you intending that the digraph relation was "directed", which gives you S4.2. $\endgroup$ Commented Mar 12, 2015 at 1:32
  • 4
    $\begingroup$ An equivalence relation on $K$ is tame if and only if it is a bisimulation between $K$ and itself. (You don’t need the frame to be reflexive or rooted for this to work.) More generally, the modal equivalence relation between two finite Kripke models is a bisimulation. (Note: “elementary” means first-order, so that’s a confusing name in this context.) You really should make yourself familiar with bisimulations and their role in modal semantics first, see e.g. the Blackburn, De Rijke, Venema textbook. $\endgroup$ Commented Mar 12, 2015 at 12:22
  • 1
    $\begingroup$ Also, $\#(K)$ will heavily depend on $K$. It can be as high as the number of all equivalence relations (e.g., if $K$ is a single cluster), which is the Bell number $B_n=((e^{-1}+o(1))n/\log n)^n$; and it can be as low as $1$ (e.g., for $K$ an irreflexive chain; if you for whatever reason insist on reflexive frames, $\#(K)=2$ for a reflexive intransitive cycle of prime length). $\endgroup$ Commented Mar 12, 2015 at 13:07

0

You must log in to answer this question.

Browse other questions tagged .