The department's research is directed to the foundations of computational models, processes and structures, and the way they support the engineering of software intensive systems. Specific areas of interest are:

When downloading papers please observe the normal copyright codes and conventions for their use.

Recent Submissions

Resolving non-determinism in choreographies

Resolving non-deterministic choices of choreographies is a crucial task. We introduce a novel notion of realisability for choreographies -called whole-spectrum implementation- that rules out deterministic implementations of roles that, no matter which context they are placed in, will never follow one of the branches of a non-deterministic choice. We show that, under some conditions, it is decidable whether an implementation is whole-spectrum. As a case study, we analyse the POP protocol under...

Bocchi, L.; Melgratti, H.; Tuosto, Emilio

Inferring Extended Finite State Machine Models from Software Executions

The ability to reverse-engineer models of software behaviour is valuable for a wide range of software maintenance, validation and verification tasks. Current reverse-engineering techniques focus either on control-specific behaviour (e.g., in the form of Finite State Machines), or data-specific behaviour (e.g., as pre / post-conditions or invariants). However, typical software behaviour is usually a product of the two; models must combine both aspects to fully represent the software's operatio...

Walkinshaw, Neil; Taylor, R.; Derrick, J.

Minimum Spanning Tree Verification under Uncertainty

In the verification under uncertainty setting, an algorithm is given, for each input item, an uncertainty area that is guaranteed to contain the exact input value, as well as an assumed input value. An update of an input item reveals its exact value. If the exact value is equal to the assumed value, we say that the update verifies the assumed value. We consider verification under uncertainty for the minimum spanning tree (MST) problem for undirected weighted graphs, where each edge is associa...

Erlebach, Thomas R.; Hoffmann, Michael

Query-competitive algorithms for cheapest set problems under uncertainty

Considering the model of computing under uncertainty where element weights are uncertain but can be obtained at a cost by query operations, we study the problem of identifying a cheapest (minimum-weight) set among a given collection of feasible sets using a minimum number of queries of element weights. For the general case we present an algorithm that makes at most d·OPT+d queries, where d is the maximum cardinality of any given set and OPT is the optimal number of queries needed to identify ...

Erlebach, Thomas; Hoffmann, Michael; Kammer, F.

Computational complexity of traffic hijacking under BGP and S-BGP

Harmful Internet hijacking incidents put in evidence how fragile the Border Gateway Protocol (BGP) is, which is used to exchange routing information between Autonomous Systems (ASes). As proved by recent research contributions, even S-BGP, the secure variant of BGP that is being deployed, is not fully able to blunt traffic attraction attacks. Given a traffic flow between two ASes, we study how difficult it is for a malicious AS to devise a strategy for hijacking or intercepting that flow. We ...

Chiesa, M.; Di Battista, G.; Patrignani, M.; Erlebach, Thomas

Approximation algorithms for disjoint st-paths with minimum activation cost

In network activation problems we are given a directed or undirected graph G = (V,E) with a family {f (x, x) : (u,v) ∈ E} of monotone non-decreasing activation functions from D to {0,1}, where D is a constant-size domain. The goal is to find activation values x for all v ∈ V of minimum total cost Σ x such that the activated set of edges satisfies some connectivity requirements. Network activation problems generalize several problems studied in the network literature such as power optimization...

Alqahtani, Hasna Mohsen; Erlebach, Thomas

Multi-Type Display Calculus for Propositional Dynamic Logic

We introduce a multi-type display calculus for Propositional Dynamic
Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnap-style
cut-elimination and subformula property.

Frittella, S.; Greco, G.; Kurz, Alexander; Palmigiano, A.

A Multi-type Display Calculus for Dynamic Epistemic Logic

In the present paper, we introduce a multi-type display calculus for dynamic
epistemic logic, which we refer to as Dynamic Calculus. The displayapproach
is suitable to modularly chart the space of dynamic epistemic logics
on weaker-than-classical propositional base. The presence of types endows
the language of the Dynamic Calculus with additional expressivity, allows
for a smooth proof-theoretic treatment, and paves the way towards a general
methodology for the design of proof systems f...

Frittella, S.; Greco, G.; Kurz, Alexander; Palmigiano, A.; Sikimić, V.

Establishing the Source Code Disruption Caused by Automated Remodularisation Tools

Current software remodularisation tools only operate on abstractions of a software system. In this paper, we investigate the actual impact of automated remodularisation on source code using a tool that automatically applies remodularisations as refactorings. This shows us that a typical remodularisation (as computed by the Bunch tool) will require changes to thousands of lines of code, spread throughout the system (typically no code files remain untouched). In a typical multi-developer projec...

Hall, M.; Khojaye, Muhammad; Walkinshaw, Neil; McMinn, P.

A Proof-Theoretic Semantic Analysis of Dynamic Epistemic Logic

The present article provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. Dynamic epistemic logic is one of the best-known members of a family of logical systems that have been successfully applied to diverse scientific disciplines, but the proof-theoretic treatment of which presents many difficulties. After an illustration of the proof-theoretic semantic principles most relevant to the treatment of logical connectives,...

Frittella, S.; Greco, G.; Kurz, Alexander H.; Palmigiano, A.; Sikimić, V.

Minimum activation cost node-disjoint paths in graphs with bounded treewidth

In activation network problems we are given a directed or undirected graph G = (V,E) with a family {f uv : (u,v) ∈ E} of monotone non-decreasing activation functions from D2 to {0,1}, where D is a constant-size subset of the non-negative real numbers, and the goal is to find activation values xv for all v ∈ V of minimum total cost ∑ v ∈ V x v such that the activated set of edges satisfies some connectivity requirements. We propose algorithms that optimally solve the minimum activation cost o...

Alqahtani, Hasna Mohsen; Erlebach, Thomas

Nominal Lambda Calculus

Since their introduction, nominal techniques have been widely applied in computer
science to reason about syntax of formal systems involving name-binding operators.
The work in this thesis is in the area of “nominal" type theory, or more precisely the
study of “nominal" simple types.
We take Nominal Equational Logic (NEL), which augments equational logic with
freshness judgements, as our starting point to introduce the Nominal Lambda Calculus
(NLC), a typed lambda calculus that provides...

Nebel, Frank

CMMI-CM compliance checking of formal BPMN models using Maude

From the perspective of business process improvement models, a business process
which is compliant with best practices and standards (e.g. CMMI) is necessary for defining
almost all types of contracts and government collaborations. In this thesis, we propose
a formal pre-appraisal approach for Capability Maturity Model Integration (CMMI)
compliance checking based on a Maude-based formalization of business processes in
Business Process Model and Notation (BPMN). The approach can be used t...

El-Saber, Nissreen A. S.

Management concerns in service-driven applications

With the abundance of functionally-similar Web-Services, the offered or agreed-on qualities are becoming decisive factors in attracting private as well as corporate customers to a given service, among all others. Nevertheless, the state-of-art in handling qualities, in this emerging service paradigm, remains largely bound to the aspects of technology and their standards (e.g. time-response, availability, throughputs). However, current approaches still ignore capital domain-based business qual...

Alghamdi, Ahmed Musfer

Flexibo : language and its application to static analysis

This thesis introduces a new object-based language FlexibO to support prototype development paradigm and more importantly, program static analysis. FlexibO offers extreme flexibility and hence enables developers to write programs that contain rich information for further analysis and optimization. FlexibO interpreter's seamless integration with Java (including direct access to Java classes and methods and direct inheritance of Java classes) makes it a suitable tool for fast prototype software...

Zhou, Jianguo

Automatic presentations of groups and semigroups

Effectively deciding the satisfiability of logical sentences over structures is an area well-studied in the case of finite structures. There has been growing work towards considering this question for infinite structures. In particular the theory of automatic structures, considered here, investigates structures representable by finite automata. The closure properties of finite automata lead naturally to algorithms for deciding satisfiability for some logics. The use of finite automata to inve...

Oliver, Graham

Formal languages and the irreducible word problem in groups

There exist structural classifications of groups with a regular, one-counter or context-free word problem. Following on from this, the main object of the work presented here has been the irreducible word problem of a group, a notion introduced by Haring-Smith, who denned it as the subset of the word problem consisting of the non-empty words which have no non-empty proper subword equal to the identity. He proved that the groups with a finite irreducible word problem with respect to some group ...

Fonseca, Ana

Optimization problems in communication networks

We study four problems arising in the area of communication networks. The minimum-weight dominating set problem in unit disk graphs asks, for a given set D of weighted unit disks, to find a minimum-weight subset D' âŠ† D such that the disks D' intersect all disks D. The problem is NP-hard and we present the first constant-factor approximation algorithm. Applying our techniques to other geometric graph problems, we can obtain better (or new) approximation algorithms. The network discovery prob...

Mihalak, Matus

Categories of containers

This thesis develops a new approach to the theory of datatypes based on separating data and storage resulting in a class of datatype called a container. The extension of a container is a functor which can be regarded as a generalised polynomial functor in type variables. A representation theorem allows every natural transformation between container functors to be represented as a unique pair of morphisms in a category.;Under suitable assumptions on the ambient category container functors are ...

Abbott, Michael Gordon

Alternative approaches to optophonic mappings

This thesis presents a number of modifications to a blind aid, known as the video optophone, which enables a blind user to more readily interpret that local environment for enhanced mobility and navigation. Versions of this form of blind aid are generally both difficult to use and interpret, and are therefore inadequate for safe mobility. The reason for this severe problem lies in the complexity and excessive bandwidth of the optophonic output after the conversion from scene-to-sound.;The w...