publications

2023

1. Compositional Automata Learning of Synchronous Systems

   Thomas Neele and Matteo Sammartino

   In Fundamental Approaches to Software Engineering - 26th International Conference (FASE), 2023

   Abs DOI

   AbstractAutomata learning is a technique to infer an automaton model of a black-box system via queries to the system. In recent years it has found widespread use both in industry and academia, as it enables formal verification when no model is available or it is too complex to create one manually. In this paper we consider the problem of learning the individual components of a black-box synchronous system, assuming we can only query the whole system. We introduce a compositional learning approach in which several learners cooperate, each aiming to learn one of the components. Our experiments show that, in many cases, our approach requires significantly fewer queries than a widely-used non-compositional algorithm such as L*.

2. Generators and Bases for Monadic Closures

   Stefan Zetzsche, Alexandra Silva, and Matteo Sammartino

   In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO), 2023

   Abs DOI

   It is well-known that every regular language admits a unique minimal deterministic acceptor. Establishing an analogous result for non-deterministic acceptors is significantly more difficult, but nonetheless of great practical importance. To tackle this issue, a number of sub-classes of non-deterministic automata have been identified, all admitting canonical minimal representatives. In previous work, we have shown that such representatives can be recovered categorically in two steps. First, one constructs the minimal bialgebra accepting a given regular language, by closing the minimal coalgebra with additional algebraic structure over a monad. Second, one identifies canonical generators for the algebraic part of the bialgebra, to derive an equivalent coalgebra with side effects in a monad. In this paper, we further develop the general theory underlying these two steps. On the one hand, we show that deriving a minimal bialgebra from a minimal coalgebra can be realized by applying a monad on an appropriate category of subobjects. On the other hand, we explore the abstract theory of generators and bases for algebras over a monad.

2022

1. Guarded Kleene Algebra with Tests: Automata Learning

   Stefan Zetzsche, Alexandra Silva, and Matteo Sammartino

   In 8th Conference on the Mathematical Foundations of Programming Semantics (MFPS), 2022

   Abs DOI

   Guarded Kleene Algebra with Tests (GKAT) is the fragment of Kleene Algebra with Tests (KAT) that arises by replacing the union and iteration operations of KAT with predicate-guarded variants. GKAT is more efficiently decidable than KAT and expressive enough to model simple imperative programs, making it attractive for applications to e.g. network verification. In this paper, we further explore GKAT’s automata theory, and present GL*, an algorithm for learning the GKAT automaton representation of a black-box, by observing its behaviour. A complexity analysis shows that it is more efficient to learn a representation of a GKAT program with GL* than with Angluin’s existing L* algorithm. We implement GL* and L* in OCaml and compare their performances on example programs.

2. ALARM: Active LeArning of Rowhammer Mitigations

   Amir Naseredini, Martin Berger, Matteo Sammartino, and 1 more author

   In 11th International Workshop on Hardware and Architectural Support for Security and Privacy (HASP), 2022

   Abs DOI

   Rowhammer is a serious security problem of contemporary dynamic random-access memory (DRAM) where reads or writes of bits can flip other bits. DRAM manufacturers add mitigations, but don’t disclose details, making it difficult for customers to evaluate their efficacy. We present a tool, based on active learning, that automatically infers parameter of Rowhammer mitigations against synthetic models of modern DRAM.

3. A Categorical Framework for Learning Generalised Tree Automata

   Gerco Heerdt, Tobias Kappé, Jurriaan Rot, and 2 more authors

   In Coalgebraic Methods in Computer Science - 16th IFIP WG 1.3 International Workshop (CMCS), 2022

   Abs DOI

   Automata learning is a popular technique used to automatically construct an automaton model from queries. Much research went into devising ad hoc adaptations of algorithms for different types of automata. The CALF project seeks to unify these using category theory in order to ease correctness proofs and guide the design of new algorithms. In this paper, we extend CALF to cover learning of algebraic structures that may not have a coalgebraic presentation. Furthermore, we provide a detailed algorithmic account of an abstract version of the popular L* algorithm, which was missing from CALF. We instantiate the abstract theory to a large class of Set functors, by which we recover for the first time practical tree automata learning algorithms from an abstract framework and at the same time obtain new algorithms to learn algebras of quotiented polynomial functors.

4. Categorical specification and implementation of Replicated Data Types

   Fabio Gadducci, Hernán C. Melgratti, Christian Roldán, and 1 more author

   Theoretical Computer Science, 2022

   Abs DOI

   Replicated Data Types (rdts) have been introduced as an abstraction for dealing with weakly consistent data stores, which may (temporarily) expose multiple, inconsistent views of their state. In the literature, rdts are usually presented in set-theoretical terms, and only recently different specification flavours have been proposed. This paper offers a categorical presentation for the specification and implementation of rdts. This paves the way for a method that allows distilling an operational semantics from a specification, which is then exploited to define a notion of implementation correctness via simulation.

5. Residuality and Learning for Nondeterministic Nominal Automata

   Joshua Moerman and Matteo Sammartino

   Logical Methods in Computer Science, 2022

   Abs DOI

   We are motivated by the following question: which data languages admit an active learning algorithm? This question was left open in previous work by the authors, and is particularly challenging for languages recognised by nondeterministic automata. To answer it, we develop the theory of residual nominal automata, a subclass of nondeterministic nominal automata. We prove that this class has canonical representatives, which can always be constructed via a finite number of observations. This property enables active learning algorithms, and makes up for the fact that residuality – a semantic property – is undecidable for nominal automata. Our construction for canonical residual automata is based on a machine-independent characterisation of residual languages, for which we develop new results in nominal lattice theory. Studying residuality in the context of nominal languages is a step towards a better understanding of learnability of automata with some sort of nondeterminism.

2021

1. Actor-based model checking for Software-Defined Networks

   Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, and 3 more authors

   Journal of Logical and Algebraic Methods in Programming, 2021

   Abs DOI PDF

   Software-Defined Networking (SDN) is a networking paradigm that has become increasingly popular in the last decade. The unprecedented control over the global behavior of the network it provides opens a range of new opportunities for formal methods and much work has appeared in the last few years on providing bridges between SDN and verification. This article advances this research line and provides a link between SDN and traditional work on formal methods for verification of concurrent and distributed software—actor-based modelling. We show how SDN programs can be seamlessly modelled using actors, and thus existing advanced model checking techniques developed for actors can be directly applied to verify a range of properties of SDN networks, including consistency of flow tables, violation of safety policies, and forwarding loops. Our model checker for SDN networks is available through an online web interface, that also provides the SDN actor-models for a number of well-known SDN benchmarks.

2020

1. Algebras for Tree Decomposable Graphs

   Roberto Bruni, Ugo Montanari, and Matteo Sammartino

   In Graph Transformation - 13th International Conference (ICGT), 2020

   Abs DOI PDF

   Complex problems can be sometimes solved efficiently via recursive decomposition strategies. In this line, the tree decomposition approach equips problems modelled as graphs with tree-like parsing structures. Following Milner’s flowgraph algebra, in a previous paper two of the authors introduced a strong network algebra to represent open graphs (up to isomorphism), so that homomorphic properties of open graphs can be computed via structural recursion. This paper extends this graphical-algebraic foundation to tree decomposable graphs. The correspondence is shown: (i) on the algebraic side by a loose network algebra, which relaxes the restriction reordering and scope extension axioms of the strong one; and (ii) on the graphical side by Milner’s binding bigraphs, and elementary tree decompositions. Conveniently, an interpreted loose algebra gives the evaluation complexity of each graph decomposition. As a key contribution, we apply our results to dynamic programming (DP). The initial statement of the problem is transformed into a term (this is the secondary optimisation problem of DP). Noting that when the scope extension axiom is applied to reduce the scope of the restriction, then also the complexity is reduced (or not changed), only so-called canonical terms (in the loose algebra) are considered. Then, the canonical term is evaluated obtaining a solution which is locally optimal for complexity. Finding a global optimum remains an NP-hard problem.

2. Residual Nominal Automata

   Joshua Moerman and Matteo Sammartino

   In 31st International Conference on Concurrency Theory (CONCUR), 2020

   Abs DOI PDF

   We are motivated by the following question: which nominal languages admit an active learning algorithm? This question was left open in previous work, and is particularly challenging for languages recognised by nondeterministic automata. To answer it, we develop the theory of residual nominal automata, a subclass of nondeterministic nominal automata. We prove that this class has canonical representatives, which can always be constructed via a finite number of observations. This property enables active learning algorithms, and makes up for the fact that residuality - a semantic property - is undecidable for nominal automata. Our construction for canonical residual automata is based on a machine-independent characterisation of residual languages, for which we develop new results in nominal lattice theory. Studying residuality in the context of nominal languages is a step towards a better understanding of learnability of automata with some sort of nondeterminism.

3. Learning Automata with Side-Effects

   Gerco Heerdt, Matteo Sammartino, and Alexandra Silva

   In Coalgebraic Methods in Computer Science - 15th International Workshop (CMCS), 2020

   Abs DOI PDF

   Automata learning has been successfully applied in the verification of hardware and software. The size of the automaton model learned is a bottleneck for scalability, and hence optimizations that enable learning of compact representations are important. This paper exploits monads, both as a mathematical structure and a programming construct, to design and prove correct a wide class of such optimizations. Monads enable the development of a new learning algorithm and correctness proofs, building upon a general framework for automata learning based on category theory. The new algorithm is parametric on a monad, which provides a rich algebraic structure to capture non-determinism and other side-effects. We show that this allows us to uniformly capture existing algorithms, develop new ones, and add optimizations.

4. Implementation correctness for Replicated Data Types, categorically

   Fabio Gadducci, Hernan Melgratti, Christian Roldan, and 1 more author

   In 17th International Colloquium on Theoretical Aspects of Computing (ICTAC), 2020

   Abs DOI PDF

   Replicated Data Types (rdts) have been introduced as an abstraction for dealing with weakly consistent data stores, which may (temporarily) expose multiple, inconsistent views of their state. In the literature, rdts are usually presented in set-theoretical terms: Only re- cently different specification flavours have been proposed, among them a denotational formalism that inter alia captures specification refinement. So far, however, no abstract model has been proposed for the implemen- tations and their correctness with respect to specifications. This paper fills the gap: We first give categorical constructions for distilling an op- erational model from a specification, as well as its implementations, and then we define a notion of implementation correctness via simulation.

2019

1. Symbolic Register Automata

   Loris D’Antoni, Tiago Ferreira, Matteo Sammartino, and 1 more author

   In 31st International Conference on Computer-Aided Verification (CAV) , 2019

   Abs DOI PDF

   Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a model over large or infinite alphabets, respectively. Both automata models have interesting applications and have been successful in their own right. In this paper, we introduce Symbolic Register Automata, a new model that combines features from both symbolic and register automata, with a view on applications that were previously out of reach. We study their properties and provide algorithms for emptiness, inclusion and equivalence checking, together with experimental results.

2. A (co)algebraic theory of succinct automata

   Gerco Heerdt, Joshua Moerman, Matteo Sammartino, and 1 more author

   Journal of Logical and Algebraic Methods in Programming, 2019

   Abs DOI PDF

   The classical subset construction for non-deterministic automata can be generalized to other side-effects captured by a monad. The key insight is that both the state space of the determinized automaton and its semantics—languages over an alphabet—have a common algebraic structure: they are Eilenberg-Moore algebras for the powersetgen monad. In this paper we study the reverse question to determinization. We will present a construction to associate succinct automata to languages based on different algebraic structures. For instance, for classical regular languages the construction will transform a deterministic automaton into a non-deterministic one, where the states represent the join-irreducibles of the language accepted by a (potentially) larger deterministic automaton. Other examples will yield alternating automata, automata with symmetries, CABA-structured automata, and weighted automata.

3. Tree Automata as Algebras: Minimisation and Determinisation

   Gerco Heerdt, Tobias Kappe, Jurriaan Rot, and 2 more authors

   In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO), 2019

   Abs DOI PDF

   We study a categorical generalisation of tree automata, as Σ-algebras for a fixed endofunctor Σendowed with initial and final states. Under mild assumptions about the base category, we present a general minimisation algorithm for these automata. We build upon and extend an existing generalisation of the Nerode equivalence to a categorical setting, and relate it to the existence of minimal automata. Lastly, we show that generalised types of side-effects, such as non-determinism, can be captured by this framework, which leads to a general determinisation procedure.

4. A Categorical Account of Replicated Data Types

   Fabio Gadducci, Hernan Melgratti, Christian Roldan, and 1 more author

   In 39th IARCS Annual Conference on. Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2019

   Abs DOI PDF

   Replicated Data Types (RDTs) have been introduced as a suitable abstraction for dealing with weakly consistent data stores, which may (temporarily) expose multiple, inconsistent views of their state. In the literature, RDTs are commonly specified in terms of two relations: visibility, which accounts for the different views that a store may have, and arbitration, which states the logical order imposed on the operations executed over the store. Different flavours, e.g., operational, axiomatic and functional, have recently been proposed for the specification of RDTs. In this work, we propose an algebraic characterisation of RDT specifications. We define categories of visibility relations and arbitrations, show the existence of relevant limits and colimits, and characterize RDT specifications as functors between such categories that preserve these additional structures.

2018

1. Decomposition Structures for Soft Constraint Evaluation Problems: An Algebraic Approach

   Ugo Montanari, Matteo Sammartino, and Alain Tcheukam Siwe

   In Graph Transformation, Specifications, and Nets, 2018

   Abs DOI PDF

   (Soft) Constraint Satisfaction Problems (SCSPs) are expressive and well-studied formalisms to represent and solve constraintsatisfaction and optimization problems. A variety of algorithms to tackle them have been studied in the last 45 years, many of them based on dynamic programming. A limit of SCSPs is its lack of compositionality and, consequently, it is not possible to represent problem decompositions in the formalism itself. In this paper we introduce Soft Constraint Evaluation Problems (SCEPs), an algebraic framework, generalizing SCSPs, which allows for the compositional specification and resolution of (soft) constraint-based problems. This enables the systematic derivation of efficient dynamic programming algorithms for any such problem.

2. SDN-Actors: Modeling and Verification of SDN Programs

   Elvira Albert, Miguel Gómez-Zamalloa, Albert Rubio, and 2 more authors

   In Formal Methods - 22nd International Symposium (FM), 2018

   Abs DOI PDF

   Software-Defined Networking (SDN) is a recent networking paradigm that has become increasingly popular in the last decade. It gives unprecedented control over the global behavior of the network and provides a new opportunity for formal methods. Much work has been published in the last few years on providing bridges between SDN and verification. This paper advances this research line and provides a link between SDN and traditional work on formal methods for verification of distributed software-actor-based modeling. We show how SDN programs can be seamlessly modeled using actors, and thus existing advanced model checking techniques are developed for use with SDN networks, including consistency of flow tables, violation of safety policies, and forwarding loops.

2017

1. CALF: Categorical Automata Learning Framework

   Gerco van Heerdt, Matteo Sammartino, and Alexandra Silva

   In 26th EACSL Annual Conference Computer Science Logics (CSL), 2017

   Abs DOI PDF

   Automata learning is a technique that has successfully been applied in verification, with the automaton type varying depending on the application domain. Adaptations of automata learning algorithms for increasingly complex types of automata have to be developed from scratch because there was no abstract theory offering guidelines. This makes it hard to devise such algorithms, and it obscures their correctness proofs. We introduce a simple category-theoretic formalism that provides an appropriately abstract foundation for studying automata learning. Furthermore, our framework establishes formal relations between algorithms for learning, testing, and minimization. We illustrate its generality with two examples: deterministic and weighted automata.

2. Learning nominal automata

   Joshua Moerman, Matteo Sammartino, Alexandra Silva, and 2 more authors

   In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017

   Abs DOI PDF

   We present an Angluin-style algorithm to learn nominal automata, which are acceptors of languages over infinite (structured) alphabets. The abstract approach we take allows us to seamlessly extend known variations of the algorithm to this new setting. In particular we can learn a subclass of nominal non-deterministic automata. An implementation using a recently developed Haskell library for nominal computation is provided for preliminary experiments.

2015

1. Revisiting causality, coalgebraically

   Roberto Bruni, Ugo Montanari, and Matteo Sammartino

   Acta Informatica, 2015

   Abs DOI PDF

   In this paper we recast the classical Darondeau–Degano’s causal semantics of concurrency in a coalgebraic setting, where we derive a compact model. Our construction is inspired by the one of Montanari and Pistore yielding causal automata, but we show that it is instance of an existing categorical framework for modeling the semantics of nominal calculi, whose relevance is further demonstrated. The key idea is to represent events as names, and the occurrence of a new event as name generation. We model causal semantics as a coalgebra over a presheaf, along the lines of the Fiore–Turi approach to the semantics of nominal calculi. More specifically, we take a suitable category of finite posets, representing causal relations over events, and we equip it with an endofunctor that allocates new events and relates them to their causes. Presheaves over this category express the relationship between processes and causal relations among the processes’ events. We use the allocation operator to define a category of well-behaved coalgebras: it models the occurrence of a new event along each transition. Then we turn the causal transition relation into a coalgebra in this category, where labels only exhibit maximal events with respect to the source states’ poset, and we show that its bisimilarity is essentially Darondeau–Degano’s strong causal bisimilarity. This coalgebra is still infinite-state, but we exploit the equivalence between coalgebras over a class of presheaves and History Dependent automata to derive a compact representation, where states only retain the poset of the most recent events for each atomic subprocess, and are isomorphic up to order-preserving permutations. Remarkably, this reduction of states is automatically performed along the equivalence.

2. Network-Conscious π-calculus - A Model of Pastry

   Ugo Montanari and Matteo Sammartino

   In Ninth Workshop on Logical and Semantic Frameworks, with Applications (LSFA), 2015

   Abs DOI PDF

   A peer-to-peer (p2p) system provides the networking substrate for the execution of distributed applications. It is made of peers that interact over an overlay network. Overlay networks are highly dynamic, as peers can join and leave at any time. Traditional process calculi, such as π-calculus, CCS and others, seem inadequate to capture these kinds of networks, their routing mechanisms, and to verify their properties. In order to model network architecture in a more explicit way, in [Ugo Montanari and Matteo Sammartino. Network conscious π-calculus: A concurrent semantics. ENTCS, 286:291–306, 2012; Matteo Sammartino. A Network-Aware Process Calculus for Global Computing and its Categorical Framework. PhD thesis, University of Pisa, 2013. available at http://www.di.unipi.it/ sammarti/publications/thesis.pdf; Ugo Montanari and Matteo Sammartino. A network-conscious π-calculus and its coalgebraic semantics. Theor. Comput. Sci., 546:188–224, 2014] we have introduced the Network Conscious π-calculus (NCPi), an extension of the π-calculus with names representing network nodes and links. In [Ugo Montanari and Matteo Sammartino. A network–conscious π-calculus and its coalgebraic semantics. Theor. Comput. Sci., 546:188–224, 2014] (a simpler version of) NCPi has been equipped with a coalgebraic operational models, along the lines of Fiore-Turi presheaf-based approach [Marcelo P. Fiore and Daniele Turi. Semantics of name and value passing. In LICS 2001, pages 93–104. IEEE Computer Society, 2001], and with an equivalent History Dependent Automaton [Ugo Montanari and Marco Pistore. Structured coalgebras and minimal hd-automata for the π-calculus. Theor. Comput. Sci., 340(3):539–576, 2005], i.e., an (often) finite-state automaton suitable for verification. In this paper we first give a brief account of these results. Then, our contribution is the sketch of a NCPi representation of the p2p architecture Pastry. In particular, we give models of its overlay network and of a Distributed Hash Table built on top of it, and we give evidence of their correctness by proving convergence of routing mechanisms.

3. A coalgebraic semantics for causality in Petri nets

   Roberto Bruni, Ugo Montanari, and Matteo Sammartino

   Journal of Logical and Algebraic Methods in Programming, 2015

   Abs DOI PDF

   In this paper we revisit some pioneering efforts to equip Petri nets with compact operational models for expressing causality. The models we propose have a bisimilarity relation and a minimal representative for each equivalence class, and they can be fully explained as coalgebras on a presheaf category on an index category of partial orders. First, we provide a set-theoretic model in the form of a causal case graph, that is a labeled transition system where states and transitions represent markings and firings of the net, respectively, and are equipped with causal information. Most importantly, each state has a poset representing causal dependencies among past events. Our first result shows the correspondence with behavior structure semantics as proposed by Trakhtenbrot and Rabinovich. Causal case graphs may be infinitely-branching and have infinitely many states, but we show how they can be refined to get an equivalent finitely-branching model. In it, states only keep the most recent causes for each token, are up to isomorphism, and are equipped with a symmetry, i.e., a group of poset isomorphisms. Symmetries are essential for the existence of a minimal, often finite-state, model. This first part requires no knowledge of category theory. The next step is constructing a coalgebraic model. We exploit the fact that events can be represented as names, and event generation as name generation. Thus we can apply the Fiore–Turi framework, where the semantics of nominal calculi are modeled as coalgebras over presheaves. We model causal relations as a suitable category of posets with action labels, and generation of new events with causal dependencies as an endofunctor on this category. Presheaves indexed by labeled posets represent the functorial association between states and their causal information. Then we define a well-behaved category of coalgebras. Our coalgebraic model is still infinite-state, but we exploit the equivalence between coalgebras over a class of presheaves and History Dependent automata to derive a compact representation, which is equivalent to our set-theoretical compact model. Remarkably, state reduction is automatically performed along the equivalence.

4. Causal Trees, Finally

   Roberto Bruni, Ugo Montanari, and Matteo Sammartino

   In Programming Languages with Applications to Biology and Security, 2015

   Abs DOI PDF

   Causal trees are one of the earliest pioneering contributions of Pierpaolo Degano, in joint work with Philippe Darondeau. The idea is to record causality dependencies in processes and in their actions. As such, causal trees sit between interleaving models and truly concurrent ones and they originate an abstract, event-based bisimulation semantics for causal processes, where, intuitively, minimal causal trees represent the semantic domain. In the paper we substantiate this feeling, by first defining a nominal, compositional operational semantics based on History-Dependent automata and then we apply categorical techniques, based on named-sets, showing that causal trees form the final coalgebra semantics of a suitable coalgebraic representation of causal behaviour.

5. Dynamic Programming on Nominal Graphs

   Nicklas Hoch, Ugo Montanari, and Matteo Sammartino

   In Graphs ad Models, 2015

   Abs DOI PDF

   Many optimization problems can be naturally represented as (hyper) graphs, where vertices correspond to variables and edges to tasks, whose cost depends on the values of the adjacent variables. Capitalizing on the structure of the graph, suitable dynamic programming strategies can select certain orders of evaluation of the variables which guarantee to reach both an optimal solution and a minimal size of the tables computed in the optimization process. In this paper we introduce a simple algebraic specification with parallel composition and restriction whose terms up to structural axioms are the graphs mentioned above. In addition, free (unrestricted) vertices are labelled with variables, and the specification includes operations of name permutation with finite support. We show a correspondence between the well-known tree decompositions of graphs and our terms. If an axiom of scope extension is dropped, several (hierarchical) terms actually correspond to the same graph. A suitable graphical structure can be found, corresponding to every hierarchical term. Evaluating such a graphical structure in some target algebra yields a dynamic programming strategy. If the target algebra satisfies the scope extension axiom, then the result does not depend on the particular structure, but only on the original graph. We apply our approach to the parking optimization problem developed in the ASCENS e-mobility case study, in collaboration with Volkswagen. Dynamic programming evaluations are particularly interesting for autonomic systems, where actual behavior often consists of propagating local knowledge to obtain global knowledge and getting it back for local decisions.

6. Reconfigurable and Software-Defined Networks of Connectors and Components

   Roberto Bruni, Ugo Montanari, and Matteo Sammartino

   2015

   Abs DOI

   The diffusion of adaptive systems motivate the study of models of software entities whose interaction capabilities can evolve dynamically. In this paper we overview the contributions in the ASCENS project in the area of software defined networks and of reconfigurable connectors. In particular we highlight: (i) the definition of the Network-conscious π-calculus and its use in the modeling and verification of the PASTRY protocol, and (ii) the mutual correspondence between different frameworks for defining networks of connectors together with two suitable enhancements for addressing dynamically changing systems.

7. From Local to Global Knowledge and Back

   Nicklas Hoch, Giacoma Valentina Monreale, Ugo Montanari, and 2 more authors

   2015

   Abs DOI

   Two forms of knowledge are considered: declarative and procedural. The former is easy to extend but it is equipped with expensive deduction mechanisms, while the latter is efficiently executable but it can hardly anticipate all the special cases. In the first part of this chapter (Sections 2 and 3), we first define a syntactic representation of Soft Constraint Satisfaction Problems (SCSPs), which allows us to express dynamic programming (DP) strategies. For the e-mobility case study of ASCENS, we use Soft Constraint Logic Programming (SCLP) to program (in CIAO Prolog) and solve local optimization problems of single electric vehicles. Then we treat the global optimization problem of finding optimal parking spots for all the cars. We provide: (i) a Java orchestrator for the coordination of local SCLP optimizations; and (ii) a DP algorithm, which corresponds to a local to global propagation and back. In the second part of this chapter (Section 4) we assume that different subjects are entitled to decide. The case study concerns a smart grid model where various prosumers (producers-consumers) negotiate (in real time, according to the DEZENT approach) the cost of the exchanged energy. Then each consumer tries to plan an optimal consumption profile (computed via DP) where (s)he uses less energy when it is expensive and more energy when it is cheap, conversely for a producer. Finally, the notion of an aggregator is introduced, whose aim is to sell flexibility to the market.

2014

1. A network-conscious π-calculus and its coalgebraic semantics

   Ugo Montanari and Matteo Sammartino

   Theoretical Computer Science, 2014

   Abs DOI PDF

   Traditional process calculi usually abstract away from network details, modeling only communication over shared channels. They, however, seem inadequate to describe new network architectures, such as Software Defined Networks, where programs are allowed to manipulate the infrastructure. In this paper we present the Network Conscious π-calculus ( NCPi), a proper extension of the π-calculus with an explicit notion of network: network links and nodes are represented as names, in full analogy with ordinary π-calculus names, and observations are routing paths through which data is transported. However, restricted links do not appear in the observations, which thus can possibly be as abstract as in the π-calculus. Then we construct a presheaf-based coalgebraic semantics for NCPi along the lines of Turi–Plotkin’s approach, by indexing processes with the network resources they use: we give a model for observational equivalence in this context, and we prove that it admits an equivalent nominal automaton (HD-automaton), suitable for verification. Finally, we give a concurrent semantics for NCPi where observations are multisets of routing paths. We show that bisimilarity for this semantics is a congruence, and this property holds also for the concurrent version of the π-calculus.

2. A Class of Automata for the Verification of Infinite, Resource-Allocating Behaviours

   Vincenzo Ciancia and Matteo Sammartino

   In 9th Symposium on Trustworthy Global Computing (TGC), 2014

   Abs DOI PDF

   Process calculi for service-oriented computing often feature generation of fresh resources. So-called nominal automata have been studied both as semantic models for such calculi, and as acceptors of languages of finite words over infinite alphabets. In this paper we investigate nominal automata that accept infinite words. These automata are a generalisation of deterministic Muller automata to the setting of nominal sets. We prove decidability of complement, union, intersection, emptiness and equivalence, and determinacy by ultimately periodic words. The key to obtain such results is to use finite representations of the (otherwise infinite-state) defined class of automata. The definition of such operations enables model checking of process calculi featuring infinite behaviours, and resource allocation, to be implemented using classical automata-theoretic methods.

2012

1. Network Conscious π-calculus: A Concurrent Semantics

   Ugo Montanari and Matteo Sammartino

   In 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS), 2012

   Abs DOI PDF

   Traditional process calculi usually abstract away from network details, modeling only communication over shared channels. They, however, seem inadequate to describe new network architectures, such as Software Defined Networks [Openflow foundation website, http://www.openflow.org/], where programs are allowed to manipulate the infrastructure. In this paper we present a network conscious, proper extension of the π-calculus: we add connector names and the primitives to handle them, and we provide a concurrent semantics. The extension to connector names is natural and seamless, since they are handled in full analogy with ordinary names. Our observations are multisets of routing paths through which sent and received data are transported. However, restricted connector names do not appear in the observations, which thus can possibly be as abstract as in the π-calculus. Finally, we show that bisimilarity is a congruence, and this property holds also for the concurrent version of the π-calculus.