Model Checking and Validity in Propositional and Modal Inclusion Logics

Model Checking and Validity in Propositional and Modal Inclusion Logics∗ Lauri Hella1, Antti Kuusisto2, Arne Meier3, and Jonni Virtema4 1 University of Tampere, Finland [email protected] 2 University of Bremen, Germany [email protected] 3 Leibniz Universität Hannover, Germany [email protected] 4 University of Helsinki, Helsinki, Finland [email protected] Abstract Propositional and modal inclusion logic are formalisms that belong to the family of logics based on team semantics. This article investigates the model checking and validity problems of these logics. We identify complexity bounds for both problems, covering both lax and strict team semantics. By doing so, we come close to finalising the programme that ultimately aims to classify the complexities of the basic reasoning problems for modal and propositional dependence, independence, and inclusion logics. 1998 ACM Subject Classification F.2 Analysis of Algorithms and Problem Complexity Keywords and phrases Inclusion Logic, Model Checking, Complexity Digital Object Identifier 10.4230/LIPIcs.MFCS.2017.32 1 Introduction Team semantics is the mathematical framework of modern logics of dependence and independence, which, unlike Tarski semantics, is not based on singletons as satisfying elements (e.g., first-order assignments or points of a Kripke structure) but on sets of such elements. More precisely, a first-order team is a set of first-order assignments that have the same domain of variables. As a result, a team can be interpreted as a database table, where variables correspond to attributes and assignments to records. Team semantics originates from the work of Hodges [ 17 ], where it was shown that Hintikka’s IF-logic can be based on a compositional (as opposed to game-theoretic) semantics. In 2007, Väänänen [ 24 ] proposed a fresh approach to logics of dependence and independence. Väänänen adopted team semantics as a core notion for his dependence logic. Dependence logic extends first-order logic by atomic statements such as the value of variable x is determined by the value of y . Such a statement is not meaningful under a single assignment, however, when evaluated over a team, such a statement corresponds precisely to functional dependence of database theory when the team is interpreted as a database table. ∗ The second and the last author acknowledges support from Jenny and Antti Wihuri Foundation. The last author is also supported by the grant 292767 of the Academy of Finland. The third author is supported by the DFG grant ME 4279/1-1. We thank the anonymous referees for their comments. ©Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema; licensed under Creative Commons License CC-BY 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Editors: Kim G. Larsen, Hans L. Bodlaender, and Jean-Francois Raskin; Article No. 32; pp. 32:1–32:14 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany 32:2 Model Checking and Validity in Propositional and Modal Inclusion Logics Besides functional dependence, there are many other important dependency notions used in fields like statistics and database theory, which give rise to interesting logics based on team semantics. The two most widely studied of these new logics are independence logic of Grädel and Väänänen [ 10 ], and inclusion logic of Galliani [ 5 ]. Inclusion logic extends first-order logic by atomic statements of the form x⊆y , which is satisfied in a team X if any value that appears as a value for x in X also appears as a value of y in X . Dependence and independence logics are equi-expressive with existential second-order logic and thus capture the complexity class NP [ 24 , 10 ]. Surprisingly, inclusion logic has the same expressive power as positive greatest fixed point logic GFP+ [ 7 ]. Since on finite structures, GFP+ coincides with least fixed point logic LFP , it follows from the Immermann-Vardi-Theorem that inclusion logic captures the complexity class Pon finite ordered structures. Interestingly under a semantical variant of inclusion logic called strict semantics the expressive power of inclusion logic rises to existential second-order logic [ 6 ]. Moreover, the fragment of inclusion logic (under strict semantics) in which only k universally quantified variables may occur captures the complexity class NTIMERAM ( nk )(i.e., structures that can be recognised by a nondeterministic random access machine in time O ( nk )) [ 11 ]. The above characterisations exemplify that, indeed, inclusion logic and its fragments have very compelling descriptive complexity-theoretic properties. In this paper, we study propositional and modal inclusion logic under both the standard semantics (i.e., lax semantics) and strict semantics. The research around propositional and modal logics with team semantics has concentrated on classifying the complexity and definability of the related logics. Due to very active research efforts, the complexity and definability landscape of these logics is understood rather well; see the survey of Durand et al. [ 4 ] and the references therein for an overview of the current state of the research. In the context of propositional logic (modal logic, resp.) a team is a set of propositional assignments with a common domain of variables (a subset of the domain a Kripke structure, resp.). Extended propositional inclusion logic (extended modal inclusion logic, resp.) extends propositional logic (modal logic, resp.) with propositional inclusion atoms ϕ⊆ψ , where ϕ and ψ are formulae of propositional logic (modal logic, resp.). Inclusion logics have fascinating properties also in the propositional setting. The following definability results hold for the standard lax semantics. A class of team pointed Kripke models is definable in extended modal inclusion logic iff ( M,∅ )is in the class for every model M , the class is closed under taking unions, and the class is closed under the so-called team k-bisimulation, for some finite k [ 16 ]. From this, a corresponding characterisation for extended propositional inclusion logic directly follows: a class of propositional teams is definable in extended propositional inclusion logic iff the empty team is in the class, and the class is closed under taking unions. In [ 21 , 22 ] (global) model definability and frame definability of team based modal logics are studied. It is shown that surprisingly, in both cases, (extended) modal inclusion logic collapses to modal logic. This paper investigates the complexity of the model checking and the validity problem for propositional and modal inclusion logic. The complexity of the satisfiability problem of modal inclusion logic was studied by Hella et al. [ 15 ]. The study on the validity problem of propositional inclusion logic was initiated by Hannula et al. [ 12 ], where the focus was on more expressive logics in the propositional setting. Consequently, the current paper directly extends the research effort initiated in these papers. It is important to note that since the logics studied in this paper are not closed under taking negations, the connection between the satisfiability problem and the validity problem fails. In [ 12 ] it was shown that, under lax semantics, the validity problem for propositional inclusion logic is coNP-complete. Here we obtain an identical result for the strict semantics. However, surprisingly, for model checking L. Hella, A. Kuusisto, A. Meier, and J. Virtema 32:3 the picture looks quite different. We establish that whereas the model checking problem for propositional inclusion logic is P-complete under lax semantics, the problem becomes NP -complete for the strict variant. Also surprisingly, for model checking in the modal setting, we obtain the identical results (as in the propositional setting): modal inclusion logic is P-complete under lax semantics and NP -complete under strict semantics. Nevertheless, for the validity problem, the modal variants are much more complex than the propositional ones; we establish coNEXP-hardness for both strict and lax semantics. 2 Propositional logics with team semantics Let D be a finite, possibly empty set of proposition symbols. A function s:D→ { 0 , 1 } is called an assignment. A set X of assignments s:D→ { 0 , 1 } is called a team. The set D is the domain of X . We denote by 2 D the set of all assignments s:D→ { 0 , 1 } . If ~p = ( p1, . . . , pn ) is a tuple of propositions and sis an assignment, we write s(~p)for (s(p1), . . . , s(pn)). Let Φbe a set of proposition symbols. The syntax of propositional logic PL (Φ) is given by the following grammar: ϕ::=p| ¬p|(ϕ∧ϕ)|(ϕ∨ϕ),where p∈Φ. We denote by | = PL the ordinary satisfaction relation of propositional logic defined via assignments in the standard way. Next we give team semantics for propositional logic. IDefinition 1 (Lax team semantics) . Let Φbe a set of atomic propositions and let X be a team. The satisfaction relation X|=ϕis defined as follows. X|=p⇔ ∀s∈X:s(p)=1, X|=¬p⇔ ∀s∈X:s(p)=0. X|= (ϕ∧ψ)⇔X|=ϕand X|=ψ. X|= (ϕ∨ψ)⇔Y|=ϕand Z|=ψ, for some Y, Z such that Y∪Z=X. The lax team semantics is considered to be the standard semantics for team-based logics. In this paper, we also consider a variant of team semantics called the strict team semantics. In strict team semantics, the above clause for disjunction is redefined as follows: X|=str (ϕ∨ψ)⇔Y|=ϕand Z|=ψ, for some Y, Z such that Y∩Z=∅and Y∪Z=X. When Ldenotes a team-based propositional logic, we let L str denote the variant of the logic with strict semantics. Moreover, in order to improve readability, for strict semantics we use | = str instead of | =. As a result lax semantics is used unless otherwise specified. The next proposition shows that the team semantics and the ordinary semantics for propositional logic defined via assignments (denoted by |=PL) coincide. IProposition 2 ([ 24 ]) . Let ϕ be a formula of propositional logic and let X be a propositional team. Then X|=ϕiff ∀s∈X:s|=PL ϕ. The syntax of propositional inclusion logic PInc (Φ) is obtained by extending the syntax of PL (Φ) by the grammar rule ϕ:: = ~p ⊆~q, where ~p and ~q are finite tuples of proposition variables with the same length. The semantics for propositional inclusion atoms is defined as follows: X|=~p ⊆~q iff ∀s∈X∃t∈X:s(~p) = t(~q). I Remark. Extended propositional inclusion logic is the variant of PInc in which inclusion atoms of the form ~ϕ ⊆~ ψ , where ~ϕ and ~ ψ are tuples of PL -formulae, are allowed. Observe that this extension does not increase the complexity of the logic and on that account, in this paper, we only consider the non-extended variant. MFCS 2017 32:4 Model Checking and Validity in Propositional and Modal Inclusion Logics p q r s1100 s2111 s3010 M: w1w2w3 s1s2s3 Figure 1 Assignments for teams in Example 4 and the Kripke model for Example 19. Table 1 Complexity of the satisfiability, validity and model checking problems for propositional logics under both systems of semantics. The shown complexity classes refer to completeness results. † In [ 15 ] NEXP -completeness is claimed. However there is a mistake in the proof and the authors of [15] now have a proof for EXP-completeness. Satisfiability Validity Model checking strict lax strict lax strict lax PL NP [3, 19] coNP [3, 19] NC1[1] PInc EXP†EXP [15] coNP [Th. 6] coNP [12] NP [Th. 14] P[Th. 10] Note that PInc is not a downward closed logic 1 . However, analogously to FO-inclusionlogic [5], satisfaction of PInc-formulas is closed under taking unions. IProposition 3 (Closure under unions) . Let ϕ∈PInc and let Xi , for i∈I , be teams. Suppose that Xi|=ϕfor each i∈I. Then Si∈IXi|=ϕ. Similarly as in first-order team semantics [ 5 ], also for propositional logic the strict and the lax semantics coincide; meaning that X| = ϕ iff X| = str ϕ for all X and ϕ . However this does not hold for propositional inclusion logic, for the following example shows that PIncstr is not union closed. Moreover, we will show that the two different semantics lead to different complexities for the related model checking problems. IExample 4. Let s1 , s2 , and s3 be as in Figure 1 and define ϕ := p∧ ( p⊆r ) ∨q∧ ( q⊆r )  . Note that {s1, s2} |=str ϕand {s2, s3} |=str ϕ, but {s1, s2, s3} 6|=str ϕ. However, PIncstr satisfies a useful weaker form of union closure: it is straightforward to prove by an induction on the formula structure that it is closed under unions of singleton teams. ILemma 5. Let X be a team and ϕ∈PIncstr . If {s} | = str ϕ for every s∈X , then X| = str ϕ . 3 Complexity of propositional inclusion logic We now define the model checking, satisfiability, and validity problems in the context of team semantics. Let Lbe a propositional logic with team semantics. A formula ϕ∈ Lis satisfiable, if there exists a non-empty team X such that X| = ϕ . A formula ϕ∈ Lis valid if X| = ϕ holds for all teams X such that the propositions in ϕ are in the domain of X . The 1 A logic Lis downward closed if “ X| = ϕ and Y⊆X implies Y| = ϕ ” holds for every formula ϕ∈ Land teams Xand Y. L. Hella, A. Kuusisto, A. Meier, and J. Virtema 32:5 satisfiability problem SAT (L)and the validity problem VAL (L)are defined in an obvious way: Given a formula ϕ∈ L, decide whether the formula is satisfiable (valid, respectively). For the model checking problem MC (L)we consider combined complexity: Given a formula ϕ∈ Land a team X , decide whether X| = ϕ . See Table 1 for known complexity results for PL and PInc, together with partial results of this paper. It was shown by Hannula et al. [ 12 ] that the validity problem of PInc is coNP -complete. Here we establish that the corresponding problem for PIncstr is also coNP -complete. Our proof is similar to theirs [12], except that instead of union closure we use Lemma 5. ITheorem 6. The validity problem for PIncstr is coNP-complete w.r.t. ≤log m. Proof Sketch. The coNP -hardness follows from the fact that PL is a sublogic of PIncstr and since the validity problem of PL is coNP -hard. On the other hand, by Lemma 5, a formula ϕ∈PIncstr is valid iff it is satisfied by all singleton teams {s} . It is easy to see that, over a singleton team {s} , any inclusion atom is equivalent to a short PL -formula. Consequently, there is a short PL -formula ϕ∗ which is valid iff ϕ is valid. Since VAL ( PL )is in coNP , the same holds for VAL(PIncstr).J 3.1 Model checking in lax semantics is P-complete In this section we construct a reduction from the monotone circuit value problem to the model checking problem of PInc. For a deep introduction to circuits see Vollmer [25]. IDefinition 7. Amonotone Boolean circuit with n input gates and one output gate is a 3-tuple C = ( V, E, α ), where ( V, E )is a finite, simple, directed, acyclic graph, and α:V→ {∨,∧, x1, . . . , xn}is a function such that the following conditions hold: 1. Every v∈Vhas in-degree 0or 2. 2. There exists exactly one w∈V with out-degree 0. We call this node w the output gate of Cand denote it by gout. 3. If v∈Vis a node with in-degree 0, then α(v)∈ {x1, . . . , xn}. 4. If v∈Vhas in-degree 2, then α(v)∈ {∨,∧}. 5. For each 1≤i≤n, there exists exactly one v∈Vwith α(v) = xi. Let C = ( V, E, α )be a monotone Boolean circuit with n input gates and one output gate. Any sequence b1, . . . , bn∈ { 0 , 1 } of bits of length n is called an input to the circuit C . A function β:V→ {0,1}defined such that β(v):=        biif α(v) = xi min β(v1), β(v2)if α(v) = ∧, where v16=v2and (v1, v),(v2, v)∈E, max β(v1), β(v2)if α(v) = ∨, where v16=v2and (v1, v),(v2, v)∈E. is called the valuation of the circuit C under the input b1, . . . , bn . The output of the circuit Cis then defined to be β(gout). The monotone circuit value problem ( MCVP ) is the following decision problem: Given a monotone circuit Cand an input b1, . . . , bn∈ {0,1}, is the output of the circuit 1? IProposition 8 ([9]).MCVP is P-complete w.r.t. ≤log mreductions. ILemma 9. MC(PInc)under lax semantics is P-hard w.r.t. ≤log m. MFCS 2017 32:6 Model Checking and Validity in Propositional and Modal Inclusion Logics Proof. We will establish a ≤log m -reduction from MCVP to the model checking problem of PInc under lax semantics. Since MCVP is P-complete, the claim follows. More precisely, we will show how to construct, for each monotone Boolean circuit C with n input gates and for each input ~ b for C , a team XC,~ b and a PInc -formula ϕC such that XC,~ b|=ϕCiff the output of the circuit Cwith the input ~ bis 1. We use teams to encode valuations of the circuit. For each gate vi of a given circuit, we identify an assignment si . The crude idea is that if si is in the team under consideration, the value of the gate vi with respect to the given input is 1. The formula ϕC is used to quantify a truth value for each Boolean gate of the circuit, and then for checking that the truth values of the gates propagate correctly. We next define the construction formally. Let C = ( V, E, α )be a monotone Boolean circuit with n input gates and one output gate and let ~ b = ( b1. . . bn ) ∈ { 0 , 1 }n be an input to the circuit C . We define that V = {v0, . . . , vm} and that v0is the output gate of C. Define τC:={p0, . . . , pm, p>, p⊥} ∪ {pk=i∨j|i < j, α(vk) = ∨,and (vi, vk),(vj, vk)∈E}. For each i≤m, we define the assignment si:τC→ {0,1}as follows: si(p):=        1if p=pior p=p>, 1if p=pk=i∨jor p=pk=j∨ifor some j, k ≤m, 0otherwise. Furthermore, we define s⊥ ( p )=1iff p = p⊥ or p = p> . We note that the assignment s⊥ will be the only assignment that maps p⊥ to 1. We make use of the fact that for each gate viof C, it holds that s⊥(pi)=0. We define XC,~ b:=si|α(vi)∈ {∧,∨}∪si|α(vi)∈ {xi|bi= 1}∪ {s⊥}, that is, XC,~ b consists of assignments for each of the Boolean gates, assignments for those input gates that are given 1as an input, and of the auxiliary assignment s⊥. Let Xbe any nonempty subteam of XC,~ bsuch that s⊥∈X. We have X|=p>⊆p0iff s0∈X X|=pi⊆pjiff (si∈Ximplies sj∈X) (1) X|=pk⊆pk=i∨jiff (i < j, (vi, vk),(vj, vk)∈E, α(vk) = ∨ and sk∈Ximplies that si∈Xor sj∈X) Recall the intuition that si∈Xshould hold iff the value of the gate viis 1. Define ψout=1 :=p>⊆p0, ψ∧:=^{pi⊆pj|(vj, vi)∈Eand α(pi) = ∧}, ψ∨:=^{pk⊆pk=i∨j|i < j, (vi, vk)∈E, (vj, vk)∈E, and α(vk) = ∨}, ϕC:=¬p⊥∨(ψout=1 ∧ψ∧∧ψ∨). Now observe that XC,~ b|=ϕCiff the output of Cwith the input ~ bis 1. The idea of the reduction is the following: The disjunction in φC is used to guess a team Y for the right disjunct that encodes the valuation β of the circuit C . The right disjunct is then evaluated with respect to the team Y with the intended meaning that β ( vi ) = 1 L. Hella, A. Kuusisto, A. Meier, and J. Virtema 32:7 whenever si∈Y . Note that Y is always as required in (1) . The formula ψout=1 is used to state that β ( v0 ) = 1, whereas the formulae ψ∧ and ψ∨ are used to propagate the truth value 1down the circuit. The assignment s⊥ and the proposition p⊥ are used as an auxiliary to make sure that Y is nonempty and to deal with the propagation of the value 0by the subformulae of the form pi⊆pj . Finally, it is easy to check that the reduction can be computed in logspace. J For the proof of the above lemma it is not important that lax semantics is considered; the same proof works also for the strict semantics. However, as we will show in the next section, we can show a stronger result for the model checking problem of PIncstr ; namely that it is NP -hard. In Section 5.1 we will show that the model checking problem for modal inclusion logic with lax semantics is in P(Lemma 21). Since PInc is essentially a fragment of this logic, by combining Lemmas 9 and 21, we obtain the following theorem. ITheorem 10. MC(PInc)under lax semantics is P-complete w.r.t. ≤log m. 3.2 Model checking in strict semantics is NP-complete In this section we reduce the set splitting problem, a well-known NP -complete problem, to the model checking problem of PIncstr. IDefinition 11. The set splitting problem is the following decision problem: Input: A family Fof subsets of a finite set S. Problem: Do there exist subsets S1and S2of Ssuch that 1. S1and S2are a partition of S(i.e., S1∩S2=∅and S1∪S2=S), 2. for each A∈ F, there exist a1, a2∈Asuch that a1∈S1and a2∈S2? IProposition 12 ([8]).The set splitting problem is NP-complete w.r.t. ≤log m. The following proof relies on the fact that strict semantics is considered. It cannot hold for lax semantics unless P=NP. ILemma 13. MC(PIncstr)is NP-hard with respect to ≤log m. Proof. We give a reduction from the set splitting problem to the model checking problem of PInc under strict semantics. Let F be an instance of the set splitting problem. We stipulate that F = {B1, . . . , Bn} and that SF = {a1, . . . , ak} , where n, k ∈N . We will introduce fresh propositions pi and qj for each point ai∈SF and set Bj∈ F . We will then encode the family of sets F by assignments over these propositions; each assignment si will correspond to a unique point ai . Formally, let τF denote the set {p1, . . . , pk, q1, . . . , qn, p>, pc, pd} of propositions. For each i∈ {1, . . . , k, c, d}, we define the assignment si:τF→ {0,1}as follows: si(p):=        1if p=pior p=p>, 1if, for some j,p=qjand ai∈Bj, 0otherwise. Define XF: = {s1, . . . , sk, sc, sd} , that is, XF consists of assignments si corresponding to each of the points ai∈SF and of two auxiliary assignments sc and sd . Note that the only assignment in XF that maps pc ( pd , resp.) to 1 is sc ( sd , resp.) and that every assignment MFCS 2017 32:8 Model Checking and Validity in Propositional and Modal Inclusion Logics maps p> to 1. Moreover, note that for 1 ≤i≤k and 1 ≤j≤n , si ( qj ) = 1 iff ai∈Bj . Now define ϕF:=¬pc∧^ i≤n p>⊆qi∨¬pd∧^ i≤n p>⊆qi. We claim that XF| = str ϕF iff the output of the set splitting problem with input F is “yes”. J In Section 5.1 we establish that the model checking problem of modal inclusion logic with strict semantics is in NP (Theorem 24). Since PIncstr is essentially a fragment of this logic, together with Lemma 13, we obtain the following theorem. ITheorem 14. MC(PIncstr)is NP-complete with respect to ≤log m. 4 Modal logics with team semantics Let Φbe a set of proposition symbols. The syntax of modal logic ML (Φ) is generated by the following grammar: ϕ:: = p| ¬p| ( ϕ∧ϕ ) | ( ϕ∨ϕ ) |♦ϕ|ϕ, where p∈Φ. By ϕ⊥ we denote the formula that is obtained from ¬ϕ by pushing all negation symbols to the atomic level using the standard duality between ∧ (  ) and ∨ ( ♦ ). A (Kripke) Φ-model is a tuple M = ( W, R, V ), where W , called the domain of M , is a non-empty set, R⊆W×W is a binary relation, and V: Φ → P ( W )is a valuation of the proposition symbols. By | = ML we denote the satisfaction relation of modal logic that is defined via pointed Φ-models in the standard way. Any subset T of the domain of a Kripke model M is called a team of M . Before we define team semantics for ML, we introduce some auxiliary notation. IDefinition 15. Let M= (W, R, V )be a model and Tand Steams of M. Define that R[T] := {w∈W| ∃v∈Ts.t. vRw}and R−1[T] := {w∈W| ∃v∈Ts.t. wRv}. For teams Tand Sof M, we write T[R]Sif S⊆R[T]and T⊆R−1[S]. Accordingly, T [ R ] S holds if and only if for every w∈T , there exists some v∈S such that wRv, and for every v∈S, there exists some w∈Tsuch that wRv. We are now ready to define team semantics for ML. IDefinition 16 (Lax team semantics) . Let M be a Kripke model and T a team of M . The satisfaction relation M, T |=ϕfor ML(Φ) is defined as follows. M, T |=p⇔w∈V(p)for every w∈T. M, T |=¬p⇔w6∈ V(p)for every w∈T. M, T |= (ϕ∧ψ)⇔M, T |=ϕand M, T |=ψ. M, T |= (ϕ∨ψ)⇔M, T1|=ϕand M, T2|=ψfor some T1and T2s.t. T1∪T2=T . M, T |=♦ϕ⇔M, T 0|=ϕfor some T0s.t. T[R]T0. M, T |=ϕ⇔M, T 0|=ϕ, where T0=R[T]. Analogously to the propositional case, we also consider the strict variant of team semantics for modal logic. In the strict team semantics, we have the following alternative semantic definitions for the disjunction and diamond (where Wdenotes the domain of M). M, T |=str (ϕ∨ψ)⇔M, T1|=ϕand M, T2|=ψ for some T1and T2such that T1∪T2=Tand T1∩T2=∅. M, T |=str ♦ϕ⇔M, f(T)|=ϕfor some f:T→Ws.t. ∀w∈T:wRf(w). L. Hella, A. Kuusisto, A. Meier, and J. Virtema 32:9 Table 2 Complexity of satisfiability, validity and model checking for modal logics under both strict and lax semantics. The given complexity classes refer to completeness results and “-h.” denotes hardness. The complexities for Minc and EMinc coincide, see Theorems 23, 24, and 26. † In [ 15 ] NEXP -completeness is claimed. However there is a mistake in the proof and the authors of [15] now have a proof for EXP-completeness. Satisfiability Validity Model checking strict lax strict lax strict lax ML PSPACE [18] PSPACE [18] P[2, 23] Minc EXP†EXP [15] coNEXP-h. [Th. 25] coNEXP-h. [Th. 25] NP [Th. 24] P[Th. 23] When Lis a team-based modal logic, we let L str to denote its variant with strict semantics. As in the propositional case, for strict semantics we use | = str instead of | =. The formulae of ML have the following flatness property. IProposition 17 (Flatness, see, e.g., [ 4 ]) . Let M be a Kripke model and T be a team of M . Then, for every formula ϕof ML(Φ):M, T |=ϕ⇔ ∀w∈T:M, w |=ML ϕ. The syntax of modal inclusion logic Minc (Φ) and extended modal inclusion logic EMinc (Φ) is obtained by extending the syntax of ML (Φ) by the following grammar rule for each n∈N : ϕ::=ϕ1, . . . , ϕn⊆ψ1, . . . , ψn, where ϕ1, ψ1, . . . , ϕn, ψn∈ML (Φ). Additionally, for Minc (Φ), we require that ϕ1 , ψ1 , . . . , ϕn , ψn are proposition symbols. The semantics for these inclusion atoms is defined as follows: M, T |=ϕ1, . . . , ϕn⊆ψ1, . . . , ψn⇔ ∀w∈T∃v∈T:^ 1≤i≤n (M,{w} |=ϕi⇔M,{v} |=ψi). The following proposition is proven in the same way as the analogous results for first-order inclusion logic [ 5 ]. A modal logic Lis union closed if M, T | = ϕ and M, S | = ϕ implies that M, T ∪S|=ϕ, for every ϕ∈L. IProposition 18 (Union Closure).The logics ML,Minc,EMinc are union closed. Analogously to the propositional case, it is easy to establish that for ML the strict and the lax semantics coincide (for a proof in the first-order setting see [ 5 ]). Again, as in the propositional case, this does not hold for Minc or EMinc . Note that since PIncstr is not union closed, neither is Mincstr, nor EMincstr. In contrary to the propositional case, Lemma 5 fails in the modal case as the following example illustrates. IExample 19. Let M be as depicted in the table of Figure 1 and let ϕ denote the PIncstr - formula of Example 4. Now M,{wi} | = str ϕ , for i∈ { 1 , 2 , 3 } , but M,{w1, w2, w3} 6| = str ϕ . 5 Model checking and validity in modal team semantics The model checking, satisfiability, and validity problems in the context of team semantics of modal logic are defined analogously to the propositional case. Let L(Φ) be a modal logic with team semantics. A formula ϕ∈ L(Φ) is satisfiable, if there exists a Kripke Φ-model MFCS 2017