We present a categorical theory of monads and distributive laws in substructural contexts. In the study of distributive laws, the roles of (the absence of) structural rules for variable contexts have been recognized; our theory formalizes these substructural situations using Tronin’s verbal categories W, in a uniform and presentation-independent manner. We introduce the classes of W-operadic monads (those defined via the structural rules in W) and of W-commutative monads (those invariant under the structural rules in W). We give a canonical construction of a distributive law ST → TS of monads on Set; it is applicable when S is W-operadic and T is W-commutative (under mild conditions). This accounts for many known and new distributive laws. Even when S fails to be W-operadic, we can refine S and force W-operadicity; this captures Varacca and Winskel’s construction of indexed valuations.

Markov decision processes (MDPs) are a popular model for decision-making in the presence of uncertainty. The conventional view of MDPs in verification treats them as state transformers with probabilities defined over sequences of states and with schedulers making random choices. An alternative view, especially well-suited for modeling dynamical systems, defines MDPs as distribution transformers with schedulers distributing probability masses. Our main contribution is a unified semantical framework that accommodates these two views and two new ones. These four semantics of MDPs arise naturally through identifying different sources of randomness in an MDP (namely schedulers, configurations, and transitions) and providing different ways of interpreting these probabilities (called the chance and mass interpretations). These semantics are systematically unified through a mathematical construct called chance-mass (CM) classifier. As another main contribution, we study a reachability problem in each of the two new semantics, demonstrating their hardness and providing two algorithms for solving them.

Algebraic Program Analysis (APA) is a ubiquitous framework that has been employed as a unifying model for various problems in data-flow analysis, termination analysis, invariant generation, predicate abstraction and a wide variety of other standard static analysis tasks. APA models program summaries as elements of a regular algebra . Suppose that a summary inAis assigned to every transition of the program and that we aim to compute the effect of running the program starting at linesand ending at linet. APA first computes a regular expression capturing all program paths of interest. In case of intraprocedural analysis, models all paths fromstot, whereas in the interprocedural case it models all interprocedurally-valid paths, i.e. ‍paths that go back to the right caller function when a callee returns. This regular expression is then interpreted over the algebra to obtain the desired result. Suppose the program hasnlines of code and each evaluation of an operation in the regular algebra takesO(k) time. It is well-known that a single APA query, or a set of queries with the same starting points, can be answered inO(n· α(n) ·k), where α is the inverse Ackermann function. In this work, we consider an on-demand setting for APA: the program is given in the input and can be preprocessed. The analysis has to then answer a large number of on-line queries, each providing a pair (s,t) of program lines which are the start and end point of the query, respectively. The goal is to avoid the significant cost of running a fresh APA instance for each query. Our main contribution is a series of algorithms that, after a lightweight preprocessing ofO(n· lgn·k), answer each query inO(k) time. In other words, our preprocessing has almost the same asymptotic complexity as a single APA query, except for a sub-logarithmic factor, and then every future query is answered instantly, i.e. ‍by a constant number of operations in the algebra. We achieve this remarkable speedup by relying on certain structural sparsity properties of control-flow and call graphs (CFGs and CGs). Specifically, we exploit the fact that control-flow graphs of real-world programs have a tree-like structure and bounded treewidth and nesting depth and that their call graphs have small treedepth in comparison to the size of the program. Finally, we provide experimental results demonstrating the effectiveness and efficiency of our approach and showing that it beats the runtime of classical APA by several orders of magnitude.