Intuitionistic Layered Graph Logic

1 Introduction

Complex systems is the field of science that studies, on the one hand, how it is that the behaviour of a system, be it natural or synthetic, derives from the behaviours of its constituent parts and, on the other, how the system interacts with its environment. A commonly employed and highly effective concept that helps to manage the difficulty in conceptualizing and reasoning about complex systems is that of layering: the system is considered to consist of a collection of interconnected layers each of which has a distinct, identifiable role in the system's operations. Layers can be informational or physical and both kinds may be present in a specific system.

Graphs provide a suitably abstract setting for a wide variety of modelling purposes, and layered graphs already form a component of existing systems modelling approaches. For example, both social networks [Br´odka et al., 2011] and transportation systems [Kurant and Thiran, 2006], have been modelled by a form of layered graph in which multiple layers are given by relations over a single set of vertices. Elsewhere layered graph models have been deployed to solve problems related to telecommunications networks [Gouveia

∗ S. Docherty and D. Pym. Intuitionistic Layered Graph Logic. Proc. IJCAR 2016, Coimbra, Portugal. LNAI 9706:469-486, 2016.

David Pym

University College London d.pym@ucl.ac.uk

et al., 2011] and to aid the design of P2P systems for businesses [Wang et al., 2009]. A bigraph [Milner, 2009] is a form of layered graph that superimposes a spatial place graph of locations and a link graph designating communication structure on a single set of vertices. Bigraphs provide models of distributed systems and have been used to generalize process models like petri nets and the π-calculus. Similar ideas have also been used to give layered models of biological systems [Maus et al., 2011].

In the present work, we give a logical analysis of the decomposition of such systems into layers, using concepts similar to ones explored with bunched logics; that is, logics that freely combine logical systems of different structural strengths. For example, the logic of bunched implications (BI) [O'Hearn and Pym, 1999; Pym et al., 2004; Galmiche et al., 2005] combines intuitionistic propositional logic [Bezhanishvili and de Jongh, 2006] with multiplicative intuitionistic linear logic [Girard, 1987]. This results in multiple coexisting conjunctions and implications with different logical properties. In particular, in BI we have both the standard conjunction ∧ and the multiplicative conjunction ∗.

This connective can be understood through an interpretation known as resource semantics. Consider a set of resources Res (ranged over by r) that is equipped with an order ⊑ and a commutative and associative operation ◦ : Res2 → Res. We think of ⊑ as a way of comparing resources and ◦ as a way of composing resources. The conjunction ∗ is then understood with the semantic clause

which is read as 'ϕ ∗ ψ holds of resource r iff it is possible to decompose part of r into disjoint resources r1 and r2 such that ϕ holds of r1 and ψ holds of r2'.

Building on this idea, we give a bunched logic suitable for reasoning about the separation of directed graphs into layers. Because of the structural properties of this decomposition we must additionally drop commutativity and associativity from the multiplicative conjunction to correctly capture it. Our work is related to a prior logic for layered graphs, LGL [Collinson et al., 2014; Collinson et al., 2015], with the key difference that our logic extends intuitionistic propositional logic rather than classical. As a consequence, we are able to prove completeness for layered graphs (rather than just for more abstract algebras) with respect to a labelled tableaux proof system, a result that (the classical) LGL lacks.

2 Layered Graphs

We first give a graph-theoretic account of the notion of layering that captures the concept as used in complex systems. Informally, two layers in a directed graph are connected by a specified set of edges, each element of which starts in the upper layer and ends in the lower layer. Our definition contrasts with prior accounts in which the layering structure is left implicit [Fiat et al., 1998; Papadimitriou and Yannakakis, 1991], and generalizes others which consider only a restricted class of layered graphs [Paz, 2011].

We begin by fixing notation and terminology. Given a directed graph, G, we refer to its vertex set by V (G). Its edge set is given by a subset E(G) ⊆ V (G) × V (G). H is a subgraph of G (H ⊆ G) iff V (H) ⊆ V (G) and E(H) ⊆ E(G). The set of subgraphs of G is denoted Sg(G).

To introduce layers, we identify a distinguished set of edges E ⊆ E(G). The reachability relation ⇝E on subgraphs of G is then defined H ⇝E K iff there exists u ∈ V (H) and v ∈ V (K) such that (u, v) ∈ E. This generates a partial composition @E on subgraphs of G. Let ↓ denote definedness. For subgraphs H and K, H@E K ↓ iff V (H) ∩ V (K) = ∅,H ⇝E K and K ̸⇝E H, with output given by the graph union of the two subgraphs and the E-edges between them. This composition is neither commutative nor - because grouping can determine definedness - associative.

Figure 1 shows subgraphs H and K for which H @E K is defined, as well as the resulting composition. We say G is a layered graph (with respect to E) if there exist H, K such that H @E K ↓ and G = H @E K. If this holds, we say H is layered over K and K is layered under H.

3 Intuitionistic Layered Graph Logic

Having established the mathematical structures we wish to reason about, we now set up intuitionistic layered graph logic (ILGL). Let Prop be a set of atomic propositions, ranged over by p. The set Form of all propositional formulae is generated by the following grammar:

The familiar connectives are interpreted as in intuitionistic propositional logic. The non-commutative and nonassociative conjunction ▶ (intended to capture layering) and its associated left and right implications ▶- - and - -▶ (cf. [Lambek, 1993]) are governed by the proof rules of Figure 2. Intuitionistic negation is defined by ¬ϕ ::= ϕ → ⊥.

ILGL is interpreted on directed graphs that have been separated into ordered layers. Formally, an ordered scaffold is a structure X = (G, E, X, ≼) such that

• E is a distinguished set of edges;
• G is a directed graph;
• X is a subset of Sg(G) satisfying: if G = H@E K then G ∈ X iff H, K ∈ X;

We consider structures that are ordered so we can extend Kripke's ordered possible world semantics of intuitionistic propositional logic [Kripke, 1965]. In Kripke's semantics, truth is persistent with respect to the order on possible worlds: if ϕ is true at a possible world x and x ≼ y, then ϕ is true at the world y. One can thus think of the intuitionistically valid propositions as those whose truth persists with the introduction of any new fact. In our setting, this means ILGL is suitable for reasoning about properties of graphs that are, for example, inherited from subgraphs, as well as modelling situations in which the components of the system carry a natural order.

• ≼ is an order on X that is reflexive and transitive.

A layered graph model M = (X , V) is given by an ordered scaffold X and a valuation V : Prop → P(X) satisfying G ∈ V(p) and G ≼ H implies H ∈ V(p). For a layered graph model M, the satisfaction relation ⊨M⊆ X × Form is inductively defined in Fig 3. ϕ is valid for a layered graph model M if, for all G ∈ X, G ⊨M ϕ. ϕ is valid if it is valid for all layered graph models M.

Consider the order given by G ≼ G′ iff G′ ⊆ G. This has a spatial interpretation: the further up the order, the more specific the location. With this order, we can understand the semantic clause for ϕ ▶ ψ as 'G is contained in a layered graph H@E K such that H satisfies ϕ and K satisfies ψ'. Similarly, the clause for ϕ-▶ψ states that 'for all subgraphs H of G, if K satisfies ϕ and is layered under H then the layered graph H@E K satisfies ψ'. Finally, ϕ▶- -ψ is the dual of the case for - -▶, with K instead layered over H.

4 A Labelled Tableaux System for ILGL

Labelled tableaux systems [Fitting, 1972] are proof calculi that have proved extremely useful in the study of bunched logics. We give a labelled tableaux system for ILGL in the style pioneered on tableaux systems for the bunched logics BBI and DMBI [Larchey-Wendling, 2014; Courtault and Galmiche, 2015] and in the spirit of previous work for BI [Galmiche et al., 2005].

The proof system centres around expressions of the form Sϕ : x, where S ∈ {T, F} is a sign (denoting true or false), ϕ is a formula of ILGL, and x is a syntactic object called a label. The set of all labels L is inductively generated from a set of atomic labels (ci)i∈N and a concatenation operation. We call expressions of the form Sϕ : x labelled formulae. We additionally define syntactic expressions x ≼ y (where x and y are labels) called constraints. Tableaux are then tree-structured derivations with labelled formulae at each node and a set of constraints associated with each branch.

The system is specified by a set of tableau expansion rules, a selection of which are given in Figure 4. The premiss of each rule gives a condition a branch must satisfy to allow the rule to be applied to it. Here F refers to the labelled formulae on the branch and C refers to the branch's associated set of constraints. The conclusion then shows how the tableau is expanded after rule application: for a conclusion 〈X, Y 〉, the branch is extended by the labelled formulae in X and the constraints in Y are added to the branch's constraint set. In cases where there are multiple conclusions - for example, 〈F ▶〉 - the branch splits.

Tableaux for a formula ϕ are defined inductively. First, the singleton tableau [Fϕ : c0] consisting of the single node Fϕ : c0 is a tableau for ϕ. Given a tableau T for ϕ, if a branch satisfies the condition of a proof rule 〈S◦〉, the tableau T ′ that results from the application of 〈S◦〉 is a tableau for ϕ.

A branch of a tableau is considered inconsistent if one of a set of predefined closure conditions is satisifed. For example, if both Tϕ : x and Fϕ : x occur on the branch. We say such a branch is closed. If all the branches of a tableau are closed, we call it a closed tableau. A tableau proof of ϕ in the labelled tableaux system is a finite closed tableau for ϕ.

This can most easily be understood through an example. Figure 5 shows a tableau proof of the formula q ▶- -(q ▶ (p → (p ∨ q))). We begin by placing the formula at the root of the tree, labelled with sign F and c0.

The labelled tableaux system for ILGL satisifies a special countermodel property: for all formulae ϕ ∈ Form, if no tableau proof exists for ϕ, then there exists a tableau with a branch that can be transformed into a layered graph model Mwith a subgraph G with the property G ̸⊨M ϕ. This is achieved by carefully specifying the permitted set of labels and the way new labels and constraints can be introduced by the tableaux rules. We then exhaustively expand the singleton tableau [Fϕ : c0] and obtain a branch in which the labels can be transformed into a directed graph that underpins a layered graph model. Satisfiablility in this model corresponds to the signs of the labelled formulae on the branch: in particular, as Fϕ : c0 occurs on the branch, the subgraph corresponding to c0 does not satisfy ϕ. Provability in the tableaux system thus captures validity for layered graph models.

At √1 , we can apply rule 〈F▶- -〉 as ▶- - is the outermost connective of the formula. This introduces the labelled formulae Tq : c2, Fq ▶ (p → (p ∨ q)) : c2c1 and adds the constraints c0 ≼ c1, c2c1 ≼ c2c1 to the branch. We next apply 〈F ▶〉 at √2 . We are able to do so because we have the constraint c2c1 ≼ c2c1 attached to the branch. This results in the branch splitting: on the left-hand side we have a closed branch because Tq : c2 and Fq : c2 both occur; on the right-hand side we have Fp → (p ∨ r) : c1. We can thus apply 〈F →〉, adding the constraint c1 ≼ c3 and the labelled formulae Tp : c3 and Fp ∨ r : c3. Lastly, we apply 〈F∨〉 at √4 , introducing Fp : c3. This closes the branch, and with it the tableau, proving q ▶- -(q ▶ (p → (p ∨ q))).

Theorem 1 (Soundness &Completeness) For all formulae ϕ ∈ Form: ϕ is valid iff there exists a tableau proof for ϕ.

5 Examples

We now give some illustrative examples to demonstrate how ILGL can be used for complex systems modelling. To do so, we assume two simple modifications to the set up of Section 3 in order to express basic notions of resource and dynamics.

First, the vertices of graphs are labelled with resources. We denote such a labelling by R, with satisfaction given on a graph together with a labelling, G[R]. This allows us to use propositional formulae to denote the presence or absence of resources on a subgraph.

Second, we assume a set of actions a for each model, each with an associated modality 〈a〉. Actions modify the resource labelling, with G[R] |=M 〈a〉ϕ iff for some labelling R′ such that a transforms R into R′ , G[R′ ] ⊨M ϕ.

Throughout, we assume the scaffolds are ordered by the following containment ordering on labelled graphs: G[R] ≼ G′ [R′ ] iff G′ ⊆ G and R ⊆ R′ . Intuitively, moving up the order gives a more precise location and a more complete assignment of resources.

5.1 A Transportation Network

Here we abstract a public transportation network into social and infrastructure layers. For a meeting in the social layer to be quorate, sufficient people (say 50) must attend. To achieve this, there must be buses of sufficient capacity to transport 50 people, represented as resources, to the meeting hall, in the infrastructure layer (see Figure 6 ) . The formula ϕquorum denotes a quorate meeting, ϕx denotes that x number of people are picked up at bus stops, and the arrival of buses of capacity x in the infrastructure layer is denoted by the action modality 〈 busx〉. These actions move x amount of people from the bus stops to the meeting hall in the social layer. Let ϕmeeting assert the existence of a meeting in the social layer, G1. Then, if G2 denotes the graph of the infrastructure layer, we have the formulae

which assert that having two buses available with a total capacity of more than 50 will allow the meeting to proceed, but that a single bus with capacity 40 will not.

5.2 A Security Barrier

This example (see Figure 7) is a situation highlighted by Schneier [Schneier, 2005], wherein a security system is ineffective because of the existence of a side-channel that allows a control to be circumvented.

The security policy, as represented in the security layer, requires that a token be possessed in order to pass from the outside to the inside; that is, 〈pass〉(ϕin → ϕtoken). However, in the routes layer it is possible to perform an action 〈swerve〉 to drive around the gate. Let G1 denote the security layer and G2 denote the routes layer. Then,

Thus we can express the mismatch between the security policy and the architecture to which it is intended to apply.

6 Conclusions &FurtherWork

We have specified a bunched logic, ILGL, for reasoning about layered graphs. The logic is sound and complete with respect to a labelled tableaux system that outputs layered graph countermodels for invalid formulae. Through a naive extension with labelled vertices and actions we have demonstrated how the logic can underpin a systems modelling framework.

While layered graphs are a key component of models of complex systems, other structure is also important. For example, in modelling the structure and dynamics of distributed systems it is necessary to capture the architecture of system locations, their associated system resources, and the processes that describe how the system delivers its services. Thus the present work represents only a first step in establishing a logical account of complex systems modelling. A second step would be to reformulate the Hennessy-Milnervan Bentham-style logics of state for location-resourceprocesses [Collinson and Pym, 2009; Collinson et al., 2012; Anderson and Pym, 2016] to incorporate layering. This would require a significantly more sophisticated notion of resource and dynamics than that given here.