SFU Theory Seminar: Eugenia Ternovska

A challenge in descriptive complexity is to identify logics with low complexity that simultaneously express both fundamental reachability properties and counting properties on unordered structures. In this talk, we introduce a family of logics that allow fine control of the complexity of order-independent computations. The approach is based on adding the ability to reason about information propagations in first-order logic with fixed points (FO(FP)). Two parameters may be used to control expressiveness and complexity: the set of definable connectives, and the expressiveness of atomic units.

We identify a fragment with polytime data complexity and show that it can express both reachability and counting properties on unordered structures. The fragment is less expressive than  FO(FP), both in its FO part and its recursive construct, but is more expressive in its ability to constrain information flows by means of (definable) modalities, similar to Dynamic logic.

We conjecture a connection of our logic to the MMSNP complexity class [Feder,Vardi:1992], which stands for Monotone Monadic Strict NP. This class has been conjectured to be a maximal fragment of NP where NP-intermediate languages are excluded. Our conjecture, if true, implies a dichotomy between PTIME and NP-complete problems definable in the logic and makes a step towards order-independent characterization of PTIME.