Theoretical Aspects of Computing - ICTAC 2015

This paper contains the informal presentation of a well known theorem on planar graphs: the theorem of Kuratowski (1930). This study is supposed to serve as an example for the proposed new discipline of

Mathematical Engineering

. The intend if this discipline is to show to informaticians, by means of examples, that there must exist important connections between rigorous mathematics and rigorous computer science. Moreover, in both cases, the mechanisation of proofs is becoming more and more fashionable these days. Such mechanisations cannot be performed without a clear understanding of the mathematical context that has to be rigorously described before engaging in the proof itself.

In this paper we report on the ongoing research of our team Comète on location privacy. In particular,we focus on the problem of protecting the privacy of the user when dealing with location-based services. The starting point of our approach is the principle of geo-indistinguishability, a formal notion of privacy that protects the user’s exact location, while allowing approximate information - typically needed to obtain a certain desired service - to be released. Then, we discuss the problem that raise in the case of traces, when the user makes consecutive uses of the location based system, while moving along a path: since the points of a trace are correlated, a simple repetition of the mechanism would cause a rapid decrease of the level of privacy. We then show a method to limit such degradation, based on the idea of predicting a point from previously reported points, instead of generating a new noisy point. Finally, we discuss a method to make our mechanism more flexible over space: we start from the observation that space is not uniform from the point of view of location hiding, and we propose an approach to adapt the level of privacy to each zone.

When a property needs to be checked against an unknown or very complex system, classical exploration techniques like modelchecking are not applicable anymore. Sometimes a monitor can be used, that checks a given property on the underlying system at runtime. A monitor for a property

L

is a deterministic finite automaton

$\mathcal{M}_L$

that after each finite execution tells whether (1) every possible extension of the execution is in

L

, or (2) every possible extension is in the complement of

L

, or neither (1) nor (2) holds. Moreover,

L

being monitorable means that it is always possible that in some future the monitor reaches (1) or (2). Classical examples for monitorable properties are safety and cosafety properties. On the other hand, deterministic liveness properties like “infinitely many a’s” are not monitorable.

We discuss various monitor constructions with a focus on deterministic

ω

-regular languages. We locate a proper subclass of deterministic

ω

-regular languages but also strictly larger than the subclass of languages which are deterministic and codeterministic; and for this subclass there exist canonical monitors which also accept the language itself.

We also address the problem to decide monitorability in comparison with deciding liveness. The state of the art is as follows. Given a Büchi automaton, it is PSPACE-complete to decide liveness or monitorability. Given an LTL formula, deciding liveness becomes EXPSPACE-complete, but the complexity to decide monitorability remains open.

As the technological and operational capabilities of unmanned aircraft systems (UAS) continue to grow, so too does the need to introduce these systems into civil airspace. Unmanned Aircraft Systems Integration in the National Airspace System is a NASA research project that addresses the integration of civil UAS into non-segregated airspace operations. One of the major challenges of this integration is the lack of an on-board pilot to comply with the legal requirement that pilots see and avoid other aircraft. The need to provide an equivalent to this requirement for UAS has motivated the development of a

detect and avoid

(DAA) capability to provide the appropriate situational awareness and maneuver guidance in avoiding and remaining well clear of traffic aircraft. Formal methods has played a fundamental role in the development of this capability. This talk reports on the formal methods work conducted under NASA’s Safe Autonomous System Operations project in support of the development of DAA for UAS. This work includes specification of low-level and high-level functional requirements, formal verification of algorithms, and rigorous validation of software implementations. The talk also discusses technical challenges in formal methods research in the context of the development and safety analysis of advanced air traffic management concepts.

This extended abstract summarises work conducted with Adrien Durier and Daniel Hirschkoff (ENS Lyon), initially reported in [38].

Bisimilarity is employed to define behavioural equivalences and reason about them. Originated in concurrency theory, bisimilarity is now widely used also in other areas, as well as outside Computer Science.

In a distributed game we imagine a team Player engaging a team Opponent in a distributed fashion. No longer can we assume that moves of Player and Opponent alternate. Rather the history of a play more naturally takes the form of a partial order of dependency between occurrences of moves. How are we to define strategies within such a game, and how are we to adjoin probability to such a broad class of strategies? The answer yields a surprisingly rich language of probabilistic distributed strategies and the possibility of programming (optimal) probabilistic strategies. Along the way we shall encounter solutions to: the need to mix probability and nondeterminism; the problem of parallel causes in which members of the same team can race to make the same move, and why this leads us to invent a new model for the semantics of distributed systems.

We present a comparative study of four product operators on weighted languages: (i) the

convolution

, (ii) the

shuffle

, (iii) the

infiltration

, and (iv) the

Hadamard

product. Exploiting the fact that the set of weighted languages is a final coalgebra, we use coinduction to prove that an operator of the classical difference calculus, the

Newton transform

, generalises (from infinite sequences) to weighted languages. We show that the Newton transform is an isomorphism of rings that transforms the Hadamard product of two weighted languages into their infiltration product, and we develop various representations for the Newton transform of a language, together with concrete calculation rules for computing them.

The delay datatype was introduced by Capretta [3] as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. It is a monad and it constitutes a constructive alternative to the maybe monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay monad quotiented by weak bisimilarity is still a monad. In this paper, we consider Hofmann’s alternative approach [6] of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. We have fully formalized our results in the Agda dependently typed programming language.

Halfway between graph transformation theory and inverse semigroup theory, we define higher dimensional strings as bi-deterministic graphs with distinguished sets of input roots and output roots. We show that these generalized strings can be equipped with an associative product so that the resulting algebraic structure is an inverse semigroup. Its natural order is shown to capture existence of root preserving graph morphism. A simple set of generators is characterized. As a subsemigroup example, we show how all finite grids are finitely generated. Finally, simple additional restrictions on products lead to the definition of subclasses with decidable Monadic Second Order (MSO) language theory.

It is a well known intuition that the exponential modality of linear logic may be seen as a form of limit. Recently, Melli‘es, Tabareau and Tasson gave a categorical account for this intuition, whereas the first author provided a topological account, based on an infinitary syntax. We relate these two different views by giving a categorical version of the topological construction, yielding two benefits: on the one hand, we obtain canonical models of the infinitary affine lambda-calculus introduced by the first author; on the other hand, we find an alternative formula for computing free commutative comonoids in models of linear logic with respect to the one presented by Melliès et al.

We present a new algorithm for active learning of register automata. Our algorithm uses counterexample-guided abstraction refinement to automatically construct a component which maps (in a history dependent manner) the large set of actions of an implementation into a small set of actions that can be handled by a Mealy machine learner. The class of register automata that is handled by our algorithm extends previous definitions since it allows for the generation of fresh output values. This feature is crucial in many real-world systems (e.g. servers that generate identifiers, passwords or sequence numbers). We have implemented our new algorithm in a tool called Tomte.

Product lines are an established framework for software design. They are specified by special diagrams called

feature models

. For formal analysis, the latter are usually encoded by propositional theories with Boolean semantics. We discuss a major deficiency of this semantics, and show that it can be fixed by considering that a product is an instantiation process rather than its final result. We call intermediate states of this process

partial

products, and argue that what a feature model

M

really defines is a poset of partial products called a

partial product line, PPL(M)

. We argue that such PPLs can be viewed as special

partial product Kripke structures

(ppKS) specifiable by a suitable version of CTL (

partial product CTL or ppCTL

). We show that any feature model

M

is representable by a ppCTL theory Φ(

M

) such that for any ppKs

K

,

K

 ⊧ Φ(

M

) iff

K

 = 

PPL

(

M

); hence, Φ(

M

) is a sound and complete representation of the feature model.

We study the determinism checking problem for regular expressions extended with interleaving. There are two notions of determinism, i.e., strong and weak determinism. Interleaving allows child elements intermix in any order. Although interleaving does not increase the expressive power of regular expressions, its use makes the sizes of regular expressions be exponentially more succinct. We first show an

$\mathcal{O}$

(| ∑ ||

E

|) time algorithm to check the weak determinism of such expressions, where ∑ is the set of distinct symbols in the expression. Next, we derive an

$\mathcal{O}$

(|

E

|) method to transform a regular expression with interleaving to its weakly star normal form which can be used to rewrite an expression that is weakly but not strongly deterministic into an equivalent strongly deterministic expression in linear time. Based on this form, we present an

$\mathcal{O}$

(| ∑ ||

E

|) algorithm to check strong determinism. As far as we know, they are the first

$\mathcal{O}$

(| ∑ ||

E

|) time algorithms proposed for solving the weak and strong determinism problems of regular expressions with interleaving.

This paper presents a novel causal semantics for concurrency, based on rigid families. Instead of having causality as primitive notion, in our model causality and concurrency are derived from precedence, a partial order local to each run of a process. We show that our causal semantics can interpret CCS and

π

-calculus terms. We propose some criteria to evaluate the correctness of a causal semantics of process calculi and we argue that none of the previous models for the

π

-calculus satisfy them all.

This is a language-theoretic investigation into a situation where a server serves an unbounded number of requests, and handling a request requires a bounded number of (arbitrarily delayed) steps. From a description of the system in interleaving semantics, one endeavours to determine whether some sequence from a given regular language is possible. We model unbounded parallelism using the iterated shuffle operator, investigate quotients of the so-called simple shuffled languages with regular languages, and prove a sufficient condition for obtaining another simple shuffled language by that operation.

Event Structures (ESs) address the representation of direct relationships between individual events, usually capturing the notions of causality and conflict. Recently, Arbach et al. introduced the new Dynamic Causality Event Structure (DCES), in which some event may change the causal dependencies of other events, by adding or dropping causal predecessors. Interestingly, DCES turned out to be incomparable— concerning their expressive power—to van Glabbeek’s and Plotkin’s Event Structure for Resolvable Conflicts (RCES), up to then considered to be one of the most general ES models.

In this paper, also motivated by process modelling in the health care domain, we present a generalisation of the DCESs, by firstly allowing sets of events for modifying dependencies, and secondly by introducing higher-order dynamics. We show that the newly defined structure is strictly more expressive than the RCESs.

We propose a variant of public announcement logic for asynchronous systems. We give a syntax where sending and receiving messages are modeled by different modal operators. The natural approach to defining the semantics leads to a circular definition, but we describe two restricted cases in which we solve this problem. The first case requires the Kripke model representing the initial epistemic situation to be a finite tree, and the second one only allows announcements from the existential fragment. Finally, we provide complexity results for the model checking problem.

A population protocol is a computational model based on pairwise interactions and designed for networks of passively mobile finite state agents. In the population protocol model, and also in the models that extend it, the interacting pairs are supposed to be chosen by a theoretical fair scheduler. In this paper, we present the

HS Scheduler

which is a totally distributed synchronous randomized handshake procedure. We then prove that this randomized handshake procedure can be a probabilistic consistent scheduler for population protocols that is fair with probability 1. By adopting a protocol aware version of the

HS Scheduler

, we introduce the

iterated population protocols

model where nodes can stop participating in the protocol’s computation once they reach a

final state

. We then study the time complexity of the computation of a particular case of this model where a

final state

is reached in only one computation step. We present some upper bounds that are later validated by simulations results.

The Quantified Constraint Satisfaction Problem (QCSP) is a generalization of classical constraint satisfaction problem in which some variables can be universally quantified. This additional expressiveness can help model problems in which a subset of the variables take value assignments that are outside the control of the decision maker. Typical examples of such domains are game-playing, conformant planning and reasoning under uncertainty. In these domains decision makers need explanations when a QCSP does not admit a winning strategy.We extend our previous approach to defining preferences amongst the requirements of a QCSP by considering more general relaxation schemes. We also present key complexity results on the hardness of finding preferred conflicts of QCSPs under this extension of the notion of preference. This paper unifies work from the fields of constraint satisfaction, explanation generation, and reasoning under preferences and uncertainty.

There exist quite a few theorems of the alternative for linear systems in the literature, with Farkas’ lemma being the most famous. All these theorems have the following form: We are given two closely related linear systems such that one and exactly one has a solution. Some specialized classes of linear systems can also be represented using graphical structures and the corresponding theorems of the alternative can then be stated in terms of properties of the graphical structure. For instance, it is well-known that a system of difference constraints (DCS) can be represented as a constraint network such that the DCS is feasible if and only if there does not exist a negative cost cycle in the network. In this paper, we provide a new graphical constraint network representation of Unit Two Variable Per Inequality (UTVPI) constraints. This constraint network representation permits us to derive a theorem of the alternative for the feasibility of UTVPI systems. UTVPI constraints find applications in a number of domains, including but not limited to program verification, abstract interpretation, and array bounds checking. Theorems of the Alternative find primary use in the design of certificates in certifying algorithms. It follows that our work is important from this perspective.

We study the strong and strutter trace distances on Markov chains (MCs). Our interest in these metrics is motivated by their relation to the probabilistic LTL-model checking problem: we prove that they correspond to the maximal differences in the probability of satisfying the same LTL and LTL

− x

(LTL without next operator) formulas, respectively. The threshold problem for these distances (whether their value exceeds a given threshold) is NP-hard and not known to be decidable. Nevertheless, we provide an approximation schema where each lower and upperapproximant is computable in polynomial time in the size of the MC.

The upper-approximants are Kantorovich-like pseudometrics, i.e. branching-time distances, that converge point-wise to the linear-time metrics. This convergence is interesting in itself, since it reveals a nontrivial relation between branching and linear-time metric-based semantics that does not hold in the case of equivalence-based semantics.

In this work, we study the interplay between monadic second order logic and the partial order theory of bounded place/transition-nets. First, we show that the causal behavior of any bounded

p

/

t

-net can be compared with respect to inclusion with the set of partial orders specified by a given MSO sentence

ϕ

. Subsequently, we address the synthesis of Petri nets from MSO specifications. More precisely, we show that given any MSO sentence

ϕ

, one can automatically construct a bounded Petri net whose behaviour minimally includes the set of partial orders specified by

ϕ

. Combining this synthesis result with the comparability results we study three problems in the realm of automated correction of faulty Petri nets, and show that these problems are decidable.

We investigate a new computational interpretation for an intuitionistic focused sequent calculus which is compatible with a resource aware semantics. For that, we associate to Herbelin’s syntax a type system based on non-idempotent intersection types, together with a set of reduction rules -inspired from the

substitution

at

a

distance

paradigm- that preserves (and decreases the size of) typing derivations. The non-idempotent approach allows us to use very simple combinatorial arguments, only based on this measure decreasingness, to characterize strongly normalizing terms by means of typability. For the sake of completeness, we also study typability (and the corresponding strong normalization characterization) in the reduction calculus obtained from the former one by projecting the explicit substitutions.

We consider (un)decidability of Multi-Lane Spatial Logic (MLSL), a multi-dimensional modal logic introduced for reasoning about traffic manoeuvres. MLSL with length measurement has been shown to be undecidable. However, the proof relies on exact values. This raises the question whether the logic remains undecidable when we consider robust satisfiability, i.e. when values are known only approximately. Our main result is that robust satisfiability of MLSL is undecidable. Furthermore, we prove that even MLSL without length measurement is undecidable. In both cases we reduce the intersection emptiness of two context-free languages to the respective satisfiability problem.

In this paper we integrate the aspect-oriented paradigm into a process algebra based component model (

$\mathcal{BRIC}$

), where correctness is guaranteed by construction. We contribute with an approach to capture, specify and use aspects to safely evolve component-based systems. We establish that components extended by aspects preserve a convergence relation that guarantees service conformance. We illustrate our results by presenting a case study of an autonomous healthcare system.

Attribute-driven software architecture design aims to provide decision support by taking into account the quality attributes of softwares. A central question in this process is:

What architecture design best fulfills the desirable software requirements?

To answer this question, a system designer needs to make tradeoffs among several potentially conflicting quality attributes. Such decisions are normally ad-hoc and rely heavily on experiences. We propose a mathematical approach to tackle this problem. Game theory naturally provides the basic language: Players represent requirements, and strategies involve setting up coalitions among the players. In this way we propose a novel model, called

decomposition game (DG)

, for attribute-driven design. We present its solution concept based on the notion of cohesion and expansion-freedom and prove that a solution always exists. We then investigate the computational complexity of obtaining a solution. The game model and the algorithms may serve as a general framework for providing useful guidance for software architecture design. We present our results through running examples and a case study on a real-life software project.

This paper presents a component-based scheme for the development of multi-rate critical embedded systems. A multi-rate system is formally specified as a modular assembly of several locally monoclocked components into a globally multi-clocked system. Mono-clocked components are modeled in particular using the synchronous programming language Quartz. Each synchronous component is first transformed into an intermediate model of clocked guarded actions. Based on the abstraction of component behaviors, consistent communication networks can be established, in which the production and consumption of inter-component dataflow are related by affine relations. Furthermore, symbolic component schedules and corresponding minimal buffering requirements are computed.

In the Android platform application security is built primarily upon a system of permissions which specify restrictions on the operations a particular process can perform. Several analyses have recently been carried out concerning the security of the Android system. Few of them, however, pay attention to the formal aspects of the permission enforcing framework. In this work we present a comprehensive formal specification of an idealized formulation of Android’s permission model and discuss several security properties that have been verified using the proof assistant Coq.

A runtime verification technique has been developed for CSP via translation of CSP models to Kripke structures. With this technique, we can check that a system under test satisfies properties of traces and refusals of its CSP model. This complements analysis facilities available for CSP and for all languages with a CSP-based semantics: Safety- Critical Java, Simulink, SysML, and so on. Soundness of the verification depends on the soundness of the translation and on the traceability of the Kripke structure analysis back to the CSP models and to the property specifications. Here, we present a formalisation of soundness by unifying the semantics of the languages involved: normalised graphs used in CSP model checking, action systems, and Kripke structures. Our contributions are the unified semantic framework and the formal argument itself.

Kademlia is the most popular peer-to-peer distributed hash table (DHT) currently in use. It offers a number of desirable features that result from the use of a notion of

distance

between objects based on the bitwise exclusive or of

n

-bit quantities that represent both nodes and files. Nodes keep information about files

close

or

near

to them in the key space and the search algorithm is based on looking for the

closest

node to the file key. The structure of the routing table defined in each peer guarantees that the lookup algorithm takes no longer than O(log(n)) steps, where

n

is the number of nodes in the network.

This paper presents a formal specification of a P2P network that uses the Kademlia DHT in the Maude language. We use sockets to connect different Maude instances and create a P2P network where the Kademlia protocol can be used, hence providing an implementation of the protocol which is correct by design. Then, we show how to abstract this system in order to analyze it by using

Real

 − 

Time

Maude

. The model is fully parameterized regarding the time taken by the different actions to facilitate the analysis of various scenarios. Finally, we use time-bounded modelchecking and exhaustive search to prove properties of the protocol over different scenarios.

This paper deals with runtime enforcement of untimed and timed properties with uncontrollable events. Runtime enforcement consists in modifying the executions of a running system to ensure their correctness with respect to a desired property. We introduce a framework that takes as input any regular (timed) property over an alphabet of events, with some of these events being uncontrollable. An uncontrollable event cannot be delayed nor intercepted by an enforcement mechanism. Enforcement mechanisms satisfy important properties, namely soundness and compliance - meaning that enforcement mechanisms output correct executions that are close to the input execution. We discuss the conditions for a property to be enforceable with uncontrollable events, and we define enforcement mechanisms that modify executions to obtain a correct output, as soon as possible. Moreover, we synthesise sound and compliant descriptions of runtime enforcement mechanisms at two levels of abstraction to facilitate their design and implementation.

We report on a tool prototype for model-based testing of cyber-physical systems. Our starting point is a hybrid-system model specified in a domain-specific language called Acumen. Our prototype tool is implemented in Matlab and covers three stages of model-based testing, namely, test-case generation, test-case execution, and conformance analysis. We have applied our implementation to a number of typical examples of cyber-physical systems in order to analyze its applicability. In this paper, we report on the result of applying the prototype tool on a DC-DC boost converter.

We present the first official release of

Caal

, a web-based tool for modelling and verification of concurrent processes. The tool is primarily designed for educational purposes and it supports the classical process algebra CCS together with its timed extension TCCS. It allows to compare processes with respect to a range of strong/weak and timed/untimed equivalences and preorders (bisimulation, simulation and traces) and supports model checking of CCS/TCCS processes against recursively defined formulae of Hennessy-Milner logic. The tool offers a graphical visualizer for displaying labelled transition systems, including their minimization up to strong/weak bisimulation, and process behaviour can be examined by playing (bi)simulation and model checking games or via the generation of distinguishing formulae for non-equivalent processes. We describe the modelling and analysis features of

Caal

, discuss the underlying verification algorithms and show a typical example of a use in the classroom environment.

Reactive Modules is a high-level specification language for concurrent and multi-agent systems, used in a number of practical model checking tools. Reactive Modules Games is a game-theoretic extension of Reactive Modules, in which concurrent agents in the system are assumed to act strategically in an attempt to satisfy a temporal logic formula representing their individual goal. The basic analytical concept for Reactive Modules Games is Nash equilibrium. In this paper, we describe a tool through which we can automatically verify Nash equilibrium strategies for Reactive Modules Games. Our tool takes as input a system, specified in the Reactive Modules language, a representation of players’ goals (expressed as CTL formulae), and a representation of players strategies; it then checks whether these strategies form a Nash equilibrium of the Reactive Modules Game passed as input. The tool makes extensive use of conventional temporal logic satisfiability and model checking techniques. We first give an overview of the theory underpinning the tool, briefly describe its structure and implementation, and conclude by presenting a worked example analysed using the tool.

Concurrent games as event structures form a partial order model of concurrency where concurrent behaviour is captured by nondeterministic concurrent strategies—a class of maps of event structures. Extended with winning conditions, the model is also able to give semantics to logics of various kinds. An interesting subclass of this game model is the one considering deterministic strategies only, where the induced model of strategies can be fully characterised by closure operators. The model based on closure operators exposes many interesting mathematical properties and allows one to define connections with many other semantic models where closure operators are also used. However, such a closure operator semantics has not been investigated in the more general nondeterministic case. Here we do so, and show that some nondeterministic concurrent strategies can be characterised by a new definition of nondeterministic closure operators which agrees with the standard game model for event structures and with its extension with winning conditions.

Having the type of all types in a type system results in paradoxes like Russel’s paradox. Therefore type theories like predicative calculus of inductive constructions (pCIC) - the logic of the Coq proof assistant - have a hierarchy of types Type

0

, Type

1

, Type

2

, . . . , where Type

0

: Type

1

, Type

1

: Type

2

, . . . . In a cumulative type system, e.g., pCIC, for a term

t

such that

t

: Type

i

we also have that

t

: Type

i

 + 1

. The system pCIC has recently been extended to support universe polymorphism, i.e., definitions can be parametrized by universe levels. This extension does not support cumulativity for inductive types. For example, we do not have that a pair of types at levels

i

and

j

is also considered a pair of types at levels

i

+ 1 and

j

+ 1.

In this paper, we discuss our on-going research on making inductive types cumulative in the pCIC. Having inductive types be cumulative alleviates some problems that occur while working with large inductive types, e.g., the category of small categories, in pCIC.

We present the pCuIC system which adds cumulativity for inductive types to pCIC and briefly discuss some of its properties and possible extensions. We, in addition, give a justification for the introduced cumulativity relation for inductive types.