Combinatorial Slice Theory

A slice is a digraph with special frontier vertices which are used to perform composition. In this thesis we introduce the foundations of a theory whose aim is to define and manipulate infinite families of combinatorial objects of a particular type, such as, graphs, partial orders, equations etc. We give special attention to families of objects that can be represented via subsets of the free monoid generated by a finite alphabet of slices. We have successfully applied our theory to obtain novel results in three fields: concurrency theory, combinatorics and logic. Some notable results are:

• We prove that inclusion and emptiness of intersection of the causal behavior of bounded Petri nets are decidable. These problems had been open for almost two decades.

• We introduce an algorithm to transitively reduce infinite families of DAGs. This algorithm allows us to operate with partial order languages defined via distinct formalisms, such as: Mazurkiewics traces, message sequence charts and step transition systems.

• We introduce the notion of z-topological order for digraphs, and use it as a point of connection between the monadic second order logic of graphs and directed width measures, such as directed path- width and cycle-rank. Through this connection we establish the polynomial time solvability of a large number of natural counting problems on digraphs admitting z-topological orderings.

• We introduce an ordered version of equational logic. We show that the validity problem for this logic is fixed parameter tractable with respect to the depth of the proof DAG, and solvable in polynomial time with respect to several notions of width of the equations ap- pearing in the proof. In this way we establish the polynomial time provability of equations that can be out of reach of techniques based on completion and heuristic search.