# What is the Upper-Bound for a Kripke Model in Normal Modal Logics?

I am currently looking for a paper for a proof about the upper-bound on the size of a Kripke model in modal logic, no matter the axiom considered.

I am considering only the propositional modal logic based on K. Thus the following set of logic :

{ K, KB, KT, K4, KBT, S4, KD4, KD, KDB } and { K5, K45, KD5, KB5, KD45, S5 }

I found many articles proposing different upper-bound according to which logic, such as:

[Sebastiani and McAllester 1997] for modal logic K, which says $Atom(phi)^{md(phi)}$ is enough to check the satisfiability of a formula.

[McKinsey,1941] for modal logic S4, which says $2^{2^{sub(phi)}}$ is enough to check the satisfiability of a formula

[Halpern and Rêgo 2007] which says that any modal logic containing Axiom (5) is bounded by $size(phi)$.

So from what I found, I have an existing bound for { K5, K45, KD5, KB5, KD45, S5 }, a bound for {K} and a bound for {S4}. Thus I still miss { KB, KT, K4, KBT, KD4, KD, KDB }

Does any of you aware of an 'universal bound'? an upper-bound on the size of the Kripke model which would be valid in all the logic that I want to consider ?

Best Regards;

[Sebastiani and McAllester 1997] Sebastiani, Roberto ; McAllester, David: New Upper Bounds for Satisfiability in Modal Logics the Case-study of Modal K / IRST, Trento, Italy. Citeseerx, October 1997. – Technical Report 9710-15. – URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.8332.

[McKinsey, 1941] J. C. C. McKinsey: A Solution of the Decision Problem for the Lewis systems {S2} and S4, with an Application to Topology, In J. Symb. Log., 6 (1941), Nr. 4, 117--134 --- URL https://doi.org/10.2307/2267105

[Halpern and Rêgo 2007] Halpern, Joseph Y. ; Rêgo, Leandro C.: Characterizing the NP- PSPACE Gap in the Satisfiability Problem for Modal Logic. In: J. Log. Comput. 17 (2007), Nr. 4, S. 795–806. – URL https://doi.org/10.1093/logcom/exm029

• Do you restrict yourself to monomodal logic or do you also consider poly-modal once? Since the latter can be undecidable and hence aren't complete w.r.t. finite models. – Daniil Kozhemiachenko Apr 11 '18 at 10:39
• I restrict myself only in the monomodal logics. – Valentin Montmirail Apr 11 '18 at 10:59
• For $\mathbf{K}_t$, i.e. minimal normal temporal logic (if this is the same as your $\mathbf{KT}$) I'd recommend to search something along the lines of “decidability of $\mathcal{ALCI}$” ($\mathcal{ALCI}$ is a description logic counterpart to polymodal $\mathbf{K}_t$). – Daniil Kozhemiachenko Apr 11 '18 at 11:18
• Well, for sure I can go and find a proof for one by one logic until I have a proof for each of them. My question is more about : does it exists an 'universal upper-bound' which works for any logic ? (in the same way as the upper-bound from Halpern & Rêgo for modal logic K*5 ?) – Valentin Montmirail Apr 11 '18 at 11:21