Analyticity, a.k.a. the subformula property, typically guarantees decidability of derivability in propositional sequent calculi. To utilize this fact, two substantial gaps have to be filled: $(i)$ what makes a sequent calculus analytic? and $(ii)$ how to obtain an efficient decision procedure for derivability in an analytic calculus? In the first part of this paper we address these gaps for \emph{pure calculi}---a general family of fully structural propositional sequent calculi whose rules allow arbitrary context formulas. We provide a sufficient syntactic criterion for analyticity in these calculi, as well as a fruitful method to construct new analytic calculi from given ones. We further introduce a scalable decision procedure for derivability in analytic pure calculi, by showing that it can be (uniformly) reduced to classical satisfiability. In the second part of the paper, we study the extension of pure sequent calculi with rules for modal operators. We show that such extensions preserve the analyticity of the calculus, and identify certain restricted operators (which we call `Next' operators) that are also amenable for a general reduction of derivability to classical satisfiability. Our proofs are all semantic, utilizing several strong general soundness and completeness theorems with respect to non-deterministic semantic frameworks: bivaluations (for pure calculi) and Kripke models (for their extension with modal operators).

Nielsen, Plotkin, and Winskel (1981) proved that every 1-safe Petri net $N$ unfolds into an event structure $\mathcal{E}_N$. By a result of Thiagarajan (1996 and 2002), these unfoldings are exactly the trace regular event structures. Thiagarajan (1996 and 2002) conjectured that regular event structures correspond exactly to trace regular event structures. In a recent paper (Chalopin and Chepoi, 2017, 2018), we disproved this conjecture, based on the striking bijection between domains of event structures, median graphs, and CAT(0) cube complexes. On the other hand, we proved that Thiagarajan's conjecture is true for regular event structures whose domains are principal filters of universal covers of (virtually) finite special cube complexes. In the current paper, we prove the converse: to any finite 1-safe Petri net $N$ one can associate a finite special cube complex ${X}_N$ such that the domain of the event structure $\mathcal{E}_N$ (obtained as the unfolding of $N$) is a principal filter of the universal cover $\widetilde{X}_N$ of $X_N$. This establishes a bijection between 1-safe Petri nets and finite special cube complexes and provides a combinatorial characterization of trace regular event structures. Using this bijection and techniques from graph theory and geometry (MSO theory of graphs, bounded treewidth, and bounded hyperbolicity) we disprove yet another conjecture by Thiagarajan (from the paper with S. Yang from 2014) that the monadic second order logic of a 1-safe Petri net is decidable if and only if its unfolding is grid-free.

Branch decomposition is a prominent method for structurally decomposing a graph, hypergraph or CNF formula. The width of a branch decomposition provides a measure of how well the object is decomposed. For many applications it is crucial to compute a branch decomposition whose width is as small as possible. We propose a SAT approach to finding branch decompositions of small width. The core of our approach is an efficient SAT encoding which determines with a single SAT-call whether a given hypergraph admits a branch decomposition of certain width. For our encoding we developed a novel partition-based characterization of branch decomposition. The encoding size imposes a limit on the size of the given hypergraph. In order to break through this barrier and to scale the SAT approach to larger instances, we developed a new heuristic approach where the SAT encoding is used to locally improve a given candidate decomposition until a fixed-point is reached. This new method scales now to instances with several thousands of vertices and edges.

This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as predicates in MAV1. The technical challenge is to establish a cut elimination result, from which essential properties including the transitivity of implication follow. Since the system is defined using the calculus of structures, a generalisation of the sequent calculus, novel techniques are employed. The proof relies on an intricately designed multiset-based measure of the size of a proof, which is used to guide a normalisation technique called splitting. The presence of equivariance, which swaps successive quantifiers, induces complex inter-dependencies between nominal quantifiers, additive conjunction and multiplicative operators in the proof of splitting. Every rule is justified by an example demonstrating why the rule is necessary for soundly embedding processes and ensuring that cut elimination holds.

This paper investigates the verification of livelock-freedom and self-stabilization on parameterized rings consisting of symmetric, constant space, deterministic and self-disabling processes. The results of this paper have a significant impact on several fields including scalable distributed systems, resilient and self-* systems, and verification of parameterized systems. First, we identify necessary and sufficient local conditions for the existence of global livelocks in parameterized unidirectional rings with unbounded (but finite) number of processes under the interleaving semantics. Using a reduction from the periodic domino problem, we show that, in general, verifying livelock-freedom of parameterized unidirectional rings is undecidable even for constant space, deterministic and self-disabling processes. This result implies that verifying self-stabilization for parameterized rings of self-disabling processes is also undecidable. We also show that verifying livelock-freedom and self-stabilization remain undecidable under (1) synchronous execution semantics; (2) the FIFO consistency model, and (3) unfair and weak scheduling policies. We then present a new scope-based method for detecting and constructing livelocks in parameterized rings. The proposed semi-algorithm behind our scope-based verification is based on a novel paradigm for the detection of livelocks that totally circumvents state space exploration. The results of this paper have significant implications for scalable distributed systems with cyclic topologies.