LRA Community:
http://hdl.handle.net/2381/316
20150303T00:37:58Z

Minimum Spanning Tree Verification under Uncertainty
http://hdl.handle.net/2381/31666
Title: Minimum Spanning Tree Verification under Uncertainty
Authors: Erlebach, Thomas R.; Hoffmann, Michael
Abstract: 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 associated with an uncertainty area and an assumed edge weight. The objective of an algorithm is to compute the smallest set of updates with the property that, if the updates of all edges in the set verify their assumed weights, the edge set of an MST can be computed. We give a polynomialtime optimal algorithm for the MST verification problem by relating the choices of updates to vertex covers in a bipartite auxiliary graph. Furthermore, we consider an alternative uncertainty setting where the vertices are embedded in the plane, the weight of an edge is the Euclidean distance between the endpoints of the edge, and the uncertainty is about the location of the vertices. An update of a vertex yields the exact location of that vertex. We prove that the MST verification problem in this vertex uncertainty setting is NPhard. This shows a surprising difference in complexity between the edge and vertex uncertainty settings of the MST verification problem.
20150213T11:59:12Z

Querycompetitive algorithms for cheapest set problems under uncertainty
http://hdl.handle.net/2381/31664
Title: Querycompetitive algorithms for cheapest set problems under uncertainty
Authors: Erlebach, Thomas; Hoffmann, Michael; Kammer, F.
Abstract: 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 (minimumweight) 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 a cheapest set. For the minimum multicut problem in trees with d terminal pairs, we give an algorithm that makes at most d·OPT+1 queries. For the problem of computing a minimumweight base of a given matroid, we give an algorithm that makes at most 2·OPT queries, generalizing a known result for the minimum spanning tree problem. For each of our algorithms we give matching lower bounds.
20150213T10:03:39Z

Computational complexity of traffic hijacking under BGP and SBGP
http://hdl.handle.net/2381/31661
Title: Computational complexity of traffic hijacking under BGP and SBGP
Authors: Chiesa, M.; Di Battista, G.; Patrignani, M.; Erlebach, Thomas
Abstract: 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 SBGP, 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 show that this problem marks a sharp difference between BGP and SBGP. Namely, while it is solvable, under reasonable assumptions, in polynomial time for the type of attacks that are usually performed in BGP, it is NPhard for SBGP. Our study has several byproducts. E.g., we solve a problem left open in the literature, stating when performing a hijacking in SBGP is equivalent to performing an interception.
20150212T15:21:43Z

Approximation algorithms for disjoint stpaths with minimum activation cost
http://hdl.handle.net/2381/31648
Title: Approximation algorithms for disjoint stpaths with minimum activation cost
Authors: Alqahtani, Hasna Mohsen; Erlebach, Thomas
Abstract: 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 nondecreasing activation functions from D to {0,1}, where D is a constantsize 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 problems. We devise an approximation algorithm for the fundamental problem of finding the Minimum Activation Cost Pair of NodeDisjoint stPaths (MA2NDP). The algorithm achieves approximation ratio 1.5 for both directed and undirected graphs. We show that a ρapproximation algorithm for MA2NDP with fixed activation values for s and t yields a ρapproximation algorithm for the Minimum Activation Cost Pair of EdgeDisjoint stPaths (MA2EDP) problem. We also study the MA2NDP and MA2EDP problems for the special case D = 2.
20150211T13:28:34Z

MultiType Display Calculus for Propositional Dynamic Logic
http://hdl.handle.net/2381/31644
Title: MultiType Display Calculus for Propositional Dynamic Logic
Authors: Frittella, S.; Greco, G.; Kurz, Alexander; Palmigiano, A.
Abstract: We introduce a multitype display calculus for Propositional Dynamic
Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnapstyle
cutelimination and subformula property.
20150211T11:12:31Z

A Multitype Display Calculus for Dynamic Epistemic Logic
http://hdl.handle.net/2381/31643
Title: A Multitype Display Calculus for Dynamic Epistemic Logic
Authors: Frittella, S.; Greco, G.; Kurz, Alexander; Palmigiano, A.; Sikimić, V.
Abstract: In the present paper, we introduce a multitype 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 weakerthanclassical propositional base. The presence of types endows
the language of the Dynamic Calculus with additional expressivity, allows
for a smooth prooftheoretic treatment, and paves the way towards a general
methodology for the design of proof systems for the generality of dynamic
logics, and certainly beyond dynamic epistemic logic. We prove that
the Dynamic Calculus adequately captures BaltagMossSolecki’s dynamic
epistemic logic, and enjoys Belnapstyle cut elimination.
20150211T11:06:46Z

Establishing the Source Code Disruption Caused by Automated Remodularisation Tools
http://hdl.handle.net/2381/31618
Title: Establishing the Source Code Disruption Caused by Automated Remodularisation Tools
Authors: Hall, M.; Khojaye, Muhammad; Walkinshaw, Neil; McMinn, P.
Editors: Poshyvanik, D.; Zaidman, A.
Abstract: 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 multideveloper project this presents a serious integration challenge, and could contribute to the low uptake of such tools in an industrial context. We relate these findings with our ongoing research into techniques that produce iterative commit friendly code changes to address this problem.
20150205T14:45:08Z

A ProofTheoretic Semantic Analysis of Dynamic Epistemic Logic
http://hdl.handle.net/2381/31596
Title: A ProofTheoretic Semantic Analysis of Dynamic Epistemic Logic
Authors: Frittella, S.; Greco, G.; Kurz, Alexander H.; Palmigiano, A.; Sikimić, V.
Editors: Aucher, G.; Hjortland, O.; Roy, O.
Abstract: The present article provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of prooftheoretic semantics. Dynamic epistemic logic is one of the bestknown members of a family of logical systems that have been successfully applied to diverse scientific disciplines, but the prooftheoretic treatment of which presents many difficulties. After an illustration of the prooftheoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display calculi, a prooftheoretic paradigm that has been successfully employed to give a prooftheoretic semantic account of modal and substructural logics. Then, we review some of the most significant proposals of proof systems for dynamic epistemic logics, and we critically reflect on them in the light of the previously introduced prooftheoretic semantic principles. The contributions of the present article include a generalization of Belnap's cutelimination metatheorem for display calculi, and a revised version of the displaystyle calculus D.EAK [30]. We verify that the revised version satisfies the previously mentioned prooftheoretic semantic principles, and show that it enjoys cutelimination as a consequence of the generalized metatheorem.
20150204T16:21:31Z

Minimum activation cost nodedisjoint paths in graphs with bounded treewidth
http://hdl.handle.net/2381/31524
Title: Minimum activation cost nodedisjoint paths in graphs with bounded treewidth
Authors: Alqahtani, Hasna Mohsen; Erlebach, Thomas
Abstract: 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 nondecreasing activation functions from D2 to {0,1}, where D is a constantsize subset of the nonnegative 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 of k nodedisjoint stpaths (stMANDP) problem in O(tw ((5 + tw)D)2tw + 2V3) time and the minimum activation cost of nodedisjoint paths (MANDP) problem for k disjoint terminal pairs (s 1,t 1),…,(s k ,t k ) in O(tw ((4 + 3tw)D)2tw + 2V) time for graphs with treewidth bounded by tw.
20150130T12:01:13Z

Nominal Lambda Calculus
http://hdl.handle.net/2381/31396
Title: Nominal Lambda Calculus
Authors: Nebel, Frank
Abstract: Since their introduction, nominal techniques have been widely applied in computer
science to reason about syntax of formal systems involving namebinding 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 a simple form of namedependent
function types. This is a key feature of NLC, which allows us to encode freshness in
a novel way.
We establish metatheoretic properties of NLC and introduce a sound model theoretic
semantics. Further, we introduce NLC[A], an extension of NLC that captures
name abstraction and concretion, and provide pure NLC[A] with a strongly
normalising and confluent βηreduction system.
A property that has not yet been studied for “nominal" typed lambda calculi is
completeness of βηconversion for a nominal analogue of full settheoretic hierarchies.
Aiming towards such a result, we analyse known proof techniques and identify various
issues. As an interesting precursor, we introduce full nominal hierarchies and
demonstrate that completeness holds for βηconversion of the ordinary typed lambda
calculus.
The notion of FMcategories was developed by Ranald Clouston to demonstrate
that FMcategories correspond precisely to NELtheories. We augment FMcategories
with equivariant exponentials and show that they soundly model NLCtheories. We
then outline why NLC is not complete for such categories, and discuss in detail an
approach towards extending NLC which yields a promising framework from which we
aim to develop a future (sound and complete) categorical semantics and a categorical
type theory correspondence.
Moreover, in pursuit of a categorical conservative extension result, we study (enriched/
internal) Yoneda isomorphisms for “nominal" categories and some form of
“nominal" gluing.
20150108T15:07:38Z

CMMICM compliance checking of formal BPMN models using Maude
http://hdl.handle.net/2381/31390
Title: CMMICM compliance checking of formal BPMN models using Maude
Authors: ElSaber, Nissreen A. S.
Abstract: 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 preappraisal approach for Capability Maturity Model Integration (CMMI)
compliance checking based on a Maudebased formalization of business processes in
Business Process Model and Notation (BPMN). The approach can be used to assess
the designed business process compliance with CMMI requirements as a step leading
to a full appraisal application. In particular, The BPMN model is mapped into Maude,
and the CMMI compliance requirements are mapped into Linear Temporal Logic (LTL)
then the Maude representation of the model is model checked against the LTL properties
using the Maude’s LTL model checker.
On the process model side, BPMN models may include structural issues that hinder
their design. In this thesis, we propose a formal characterization and semantics specification
of wellformed BPMN processes using the formalization of rewriting logic (Maude)
with a focus on databased decision gateways and data objects semantics. Our formal
specification adheres to the BPMN standards and enables model checking using Maude’s
LTL model checker. The proposed semantics is formally proved to be sound based on the
classical workflow model soundness definition. On the compliance requirements side,
CMMI configuration management process is used as a source of compliance requirements
which then are mapped through compliance patterns into LTL properties. Model
checking results of Maude based implementation are explained based on a compliance
grading scheme. Examples of CMMI configuration management processes are used to
illustrate the approach.
20150108T12:29:00Z

Management concerns in servicedriven applications
http://hdl.handle.net/2381/30107
Title: Management concerns in servicedriven applications
Authors: Alghamdi, Ahmed Musfer
Abstract: With the abundance of functionallysimilar WebServices, the offered or agreedon qualities are becoming decisive factors in attracting private as well as corporate customers to a given service, among all others. Nevertheless, the stateofart in handling qualities, in this emerging service paradigm, remains largely bound to the aspects of technology and their standards (e.g. timeresponse, availability, throughputs). However, current approaches still ignore capital domainbased business qualities and management concerns (e.g. customer profiles, business deadlines). The main objective of this thesis is to leverage the handling of quality and management issues in servicedriven business applications toward the intuitive business level supported by a precise and flexible conceptualisation. Thus, instead of addressing qualities using just rigid ITSLA (servicelevel agreements) as followed by Web Services technology and standards, we propose to cope with more abstract and domaindependent and adaptive qualities in an intuitive, yet conceptual, manner. The approach is centred on evolving business rules and policies for management, with a clean separation of functionalities as specific rules. At the conceptual level, we propose specialised architectural connectors called management laws that we also separate from coordination laws for functionality issues. We further propose a smooth and compliant mapping of the conceptualisation toward service technology, using existing rulebased standards.
20141215T10:36:12Z

Flexibo : language and its application to static analysis
http://hdl.handle.net/2381/30106
Title: Flexibo : language and its application to static analysis
Authors: Zhou, Jianguo
Abstract: This thesis introduces a new objectbased 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 development. FlexibO's extreme flexibility allows developers to redefine the behavior of program evaluation by overriding its default evaluation method. This mechanism can be used to translate FlexibO to other efficient languages. In this thesis we design a translator in FlexibO to translate BulkSynchronous Parallel specifications (expressed in FlexibO) to executable C pro grams linked with BSPLib. Before translation, the tool first checks syntax and type, then statically analyzes potential communication conflicts, and finally generates C code. The translation process can accurately analyze primitive commands but require approximation (using abstract interpretation) for more advanced commands such as loops. The appropriateness of the translator and the associated static analysis can be formally analyzed using the technique of normal form.
20141215T10:36:12Z

Automatic presentations of groups and semigroups
http://hdl.handle.net/2381/30105
Title: Automatic presentations of groups and semigroups
Authors: Oliver, Graham
Abstract: Effectively deciding the satisfiability of logical sentences over structures is an area wellstudied 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 investigate infinite structures has been inspired by the interplay between the theory of finite automata and the theory of semigroups. This inspiration has come in particular from the theory of automatic groups and semigroups, which considers (semi)groups with regular sets of normal forms over their generators such that generatorcomposition is also regular. The work presented here is a contribution to the foundational problem for automatic structures: given a class of structures, classify those members that have an automatic presentation. The classes considered here are various interesting subclasses of the class of finitely generated semigroups, as well as the class of Cayley Graphs of groups. Although similar, the theories of automatic (semi)groups and automatic presentation differ in their construction. A classification for finitely generated groups allows a direct comparison of the theory of automatic presentations with the theory of automatic groups.
20141215T10:36:10Z

Formal languages and the irreducible word problem in groups
http://hdl.handle.net/2381/30103
Title: Formal languages and the irreducible word problem in groups
Authors: Fonseca, Ana
Abstract: There exist structural classifications of groups with a regular, onecounter or contextfree 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 HaringSmith, who denned it as the subset of the word problem consisting of the nonempty words which have no nonempty proper subword equal to the identity. He proved that the groups with a finite irreducible word problem with respect to some group generating set are exactly the plain groups.;We know that the class of groups with a contextfree irreducible word problem is a proper subclass of the virtually free groups. We look at direct products of finitely generated free groups by finite groups and also at the plain groups and consider their irreducible word problems with respect to minimal group generating sets. We prove that, of all the direct products of the infinite cyclic group by a nontrivial finite group, only Z x Z2 and Z x Z 3 have contextfree irreducible word problem (and only with respect to a few group generating sets). We also exhibit a plain group that has contextfree irreducible word problem with respect to every minimal group generating set.;Looking at the direct products of finitely generated free groups by nontrivial finite groups, we have found that the only irreducible word problem that is onecounter is that of Z x Z2 with respect to the canonical group generating set.;As for irreducible word problems lying in classes of languages above contextfree, on one hand, we prove that having a recursive irreducible word problem is equivalent to having a recursive word problem. On the other hand, we prove that, while there are groups such that the fact that their irreducible word problem is recursively enumerable implies that they are recursive, that is not always the case.
20141215T10:36:09Z

Optimization problems in communication networks
http://hdl.handle.net/2381/30104
Title: Optimization problems in communication networks
Authors: Mihalak, Matus
Abstract: We study four problems arising in the area of communication networks. The minimumweight dominating set problem in unit disk graphs asks, for a given set D of weighted unit disks, to find a minimumweight subset D' âŠ† D such that the disks D' intersect all disks D. The problem is NPhard and we present the first constantfactor approximation algorithm. Applying our techniques to other geometric graph problems, we can obtain better (or new) approximation algorithms. The network discovery problem asks for a minimum number of queries that discover all edges and nonedges of an unknown network (graph). A query at node v discovers a certain portion of the network. We study two different query models and show various results concerning the complexity, approximability and lower bounds on competitive ratios of online algorithms. The OVSFcode assignment problem deals with assigning communication codes (nodes) from a complete binary tree to users. Users ask for codes of a certain depth and the codes have to be assigned such that (i) no assigned code is an ancestor of another assigned code and (ii) the number of (previously) assigned codes that have to be reassigned (in order to satisfy (i)) is minimized. We present hardness results and several algorithms (optimal, approximation, online and fixedparameter tractable). The joint base station scheduling problem asks for an assignment of users to base stations (points in the plane) and for an optimal colouring of the resulting conflict graph: user u with its assigned base station b is in conflict with user v, if a disk with center at 6, and u on its perimeter, contains v. We study the complexity, and present and analyse optimal, approximation and greedy algorithms for general and various special cases.
20141215T10:36:09Z

Categories of containers
http://hdl.handle.net/2381/30102
Title: Categories of containers
Authors: Abbott, Michael Gordon
Abstract: 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 closed under composition, limits, coproducts and the construction of initial algebras and final coalgebras. These closure properties allow containers to provide a functorial semantics for an important class of polymorphic types including the strictly positive types.;Since polymorphic functions between functorial polymorphic types correspond to natural transformations, every polymorphic function can be represented as a container morphism; this simplifies reasoning about such functions and provides a framework for developing concepts of generic programming.;Intuitionistic wellfounded trees or Wtypes are the initial algebras of container functors in one parameter; the construction of the initial algebra of a container in more than one parameter leads to the solution of a problem left incomplete by earlier work of Dybjer.;We also find that containers provide a suitable framework to define the derivative of a functor as a kind of linear exponential. We show that the use of containers is essential for this approach.;The theory is developed in the context of a fairly general category to allow for a wide choice of applications. We use the language of dependent type theory to develop the theory of containers in an arbitrary extensive locally cartesian closed category; much of the development in this thesis can also be generalised to display map categories. We develop the appropriate internal language and its interpretation in a category with families.
20141215T10:36:09Z

Alternative approaches to optophonic mappings
http://hdl.handle.net/2381/30101
Title: Alternative approaches to optophonic mappings
Authors: Capp, Michael.
Abstract: 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 scenetosound.;The work herein describes a number of modifications that can be applied to the current optophonic process to make more efficient use of the limited bandwidth provided by the auditory system when converting scene images to sound. Various image processing and stereo techniques have been employed to artificially emulate the human visual system through the use of depth maps that successfully fade out the quantity of relatively unimportant image features, whilst emphasising the more significant regions such as nearby obstacles.;A series of experiments was designed to test these various modifications to the optophonic mapping by studying important factors of mobility and subject response whilst going about everyday life. The devised system, labelled DeLIA for the Detection, Location, Identification, and Avoidance (or Action) of obstacles, provided a means for gathering statistical data on users' interpretation of the optophonic output. An analysis of this data demonstrated a significant improvement when using the stereo cartooning technique, developed as part of this work, over the more conventional plain image as an input to an optophonic mapping from scenetosound.;Lastly, conclusions were drawn from the results, which indicated that the use of a stereo depth map as an input to a video optophone would improve its usefulness as an aid to general mobility. For the purposes of detecting and determining text or similar detail, either a plain unmodified image or some form of edge (depth) image were found to produce the best results.
20141215T10:36:08Z

Multimodal humancomputer interaction for enhancing customers’ decisionmaking and experience on B2C ecommerce websites
http://hdl.handle.net/2381/29330
Title: Multimodal humancomputer interaction for enhancing customers’ decisionmaking and experience on B2C ecommerce websites
Authors: Al Sokkar, Abdullah Ahmad Musa
Abstract: The main aim of this thesis was to identify, complement and refine the factors that contribute to users’ intention to purchase, satisfaction and attitude toward using a particular B2C online environment, as well as the causal relationships between these factors. A systematic literature review on Information System (IS), Market Research, and User Experience (UX), which has informed the design and development of a pilot study, has been conducted. Results have led to the conception of an online shopping decisionmaking (OSDM) model called ‘Episodic UX Model on DecisionMaking’ (EUXDM). It has been developed by integrating the established Technology Acceptance Model (TAM) as well as Information System Success Model (ISSM), and emerging UX models, and ExpectationConfirmation Theory (ECT). Results from analysing 305 responses to the webbased questionnaire aimed to evaluate EUXDM verified its validity. In addition, after investigating the users’ preferences for the possible modifications related to the use of visual avatar in a particular B2C eCommerce website for information presentation, another research focus has been placed on identifying the real conversational functions and their related communicational behaviour in designing male and female visual avatars’ facial expressions and body gestures. Following this, four different types of information presentations have been developed to be used in a contrived B2C online shopping environment, namely: (i) 2D static graphical and textual information, (ii) nonexpressive avatars, (iii) avatars with facial expressions, (iv) and avatars with facial expressions and body gestures information presentations. Consequently, these information presentations were empirically investigated through two experimental studies. The outcomes of these studies indicated that the gender of the avatar and participants were found to be insignificant factors for any of the measured qualities, and the use of visual avatars with animated facial expressions and body gestures positively influenced customers’ usage attitude, intention to purchase and satisfaction.
20141209T11:49:14Z

Lem : Reusable engineering of realworld semantics
http://hdl.handle.net/2381/29328
Title: Lem : Reusable engineering of realworld semantics
Authors: Mulligan, Dominic P.; Gray, Kathryn E.; Sewell, Peter; Owens, Scott; Ridge, Tom
Abstract: Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous semantic models (not just idealised calculi) of realworld processors, programming languages, protocols, and security mechanisms, for testing, proof, analysis, and design. Building these models is challenging, requiring experimentation, dialogue with vendors or standards bodies, and validation; their scale adds engineering issues akin to those of programming to the task of writing clear and usable mathematics. But language and tool support for specification is lacking. Proof assistants can be used but bring their own difficulties, and a model produced in one, perhaps requiring many personyears effort and maintained over an extended period, cannot be used by those familiar with another. We introduce Lem, a language for engineering reusable largescale semantic models. The Lem design takes inspiration both from functional programming languages and from proof assistants, and Lem definitions are translatable into OCaml for testing, Coq, HOL4, and Isabelle/HOL for proof, and LaTeX and HTML for presentation. This requires a delicate balance of expressiveness, careful library design, and implementation of transformations  akin to compilation, but subject to the constraint of producing usable and humanreadable code for each target. Lem's effectiveness is demonstrated by its use in practice. © 2014 ACM.
20141209T10:33:34Z

Simple, efficient, sound and complete combinator parsing for all contextfree grammars, using an oracle
http://hdl.handle.net/2381/29327
Title: Simple, efficient, sound and complete combinator parsing for all contextfree grammars, using an oracle
Authors: Ridge, Tom
Abstract: Parsers for contextfree grammars can be implemented directly and naturally in a functional style known as “combinator parsing”, using recursion following the structure of the grammar rules. Traditionally parser combinators have struggled to handle all features of contextfree grammars, such as left recursion.
Previous work introduced novel parser combinators that could be used to parse all contextfree grammars. A parser generator built using these combinators was proved both sound and complete in the HOL4 theorem prover. Unfortunately the performance was not as good as other parsing methods such as Earley parsing.
In this paper, we build on this previous work, and combine it in novel ways with existing parsing techniques such as Earley parsing. The result is a soundandcomplete combinator parsing library that can handle all contextfree grammars, and has good performance.
Description: timestamp: Tue, 09 Sep 2014 10:57:11 +0200 biburl: http://dblp.unitrier.de/rec/bib/conf/sle/Ridge14 bibsource: dblp computer science bibliography, http://dblp.org
20141209T10:20:37Z

On the Synthesis of Choreographies
http://hdl.handle.net/2381/29310
Title: On the Synthesis of Choreographies
Authors: Lange, Julien
Abstract: The theories based on session types stand out as effective methodologies
to specify and verify properties of distributed systems. A key result in the area shows the
suitability of choreography languages and session types as a basis for a choreographydriven
methodology for distributed software development. The methodology it advocates
is as follows: a team of programmers designs a global view of the interactions to be
implemented (i.e., a choreography), then the choreography is projected onto each role.
Finally, each program implementing one or more roles in the choreography is validated
against its corresponding projection(s).
This is an ideal methodology but it may not always be possible to design one set of
choreographies that will drive the overall development of a distributed system. Indeed,
software needs maintenance, specifications may evolve (sometimes also during the development),
and issues may arise during the implementation phase. Therefore, there is a
need for an alternative approach whereby it is possible to infer a choreography from local
behavioural specifications (i.e., session types).
We tackle the problem of synthesising choreographies from local behavioural specifications
by introducing a type system which assigns – if possible – a choreography to
set of session types. We demonstrate the importance of obtaining a choreography from
local specifications through two applications. Firstly, we give three algorithms and a
methodology to help software designers refine a choreography into a global assertion,
i.e., a choreography decorated with logical formulae specifying senders’ obligations and
receivers’ requirements. Secondly, we introduce a formal model for distributed systems
where each participant advertises its requirements and obligations as behavioural contracts
(in the form of session types), and where multiparty sessions are started when a set
of contracts allows to synthesise a choreography.
20141204T12:10:48Z

User Activity Recognition through Software Sensors
http://hdl.handle.net/2381/29228
Title: User Activity Recognition through Software Sensors
Authors: ReiffMarganiec, Stephan
Abstract: Contextaware systems are an instance of the ubiquitous or pervasive computing vision. They sense the users’ physical and virtual surrounding to identify the best system support for that user and adapt the system behaviour accordingly. The overall architecture of a context aware system can be broken into a number of logical aspects: gathering context data, storing the data, deriving knowledge through reasoning and mining and retrieving that knowledge to finally adapting system behaviours. Context is anything characterizing the environment of the user – their location, the ambient temperature, the people they are with, their current activity and some even consider the user’s mood. Traditionally context information has been gathered through the use of hardware sensors, such as GPS sensors or smart badges for locations and there has been work to track user’s eye movements at their desk to see which application they are using. However, determining the activity of a user has shown to be elusive to being sensed with hardware sensors. As users use web services more frequently they are exchanging messages with the services through the SOAP protocol. SOAP messages contain data, which is valuable if gathered and interpreted right – especially as this data can be shedding information on the activity of a user that goes beyond “sitting at the computer and typing”. We propose a complimentary sensor technology through the use of software sensors. The software sensors are essentially based on monitoring SOAP messages and inserting data for further reasoning and querying into a semantic context model. In this paper we consider details of extracting the data from SOAP messages in a nonobstructive way and show a solution to map the data from a SOAP message to our OWL ontology model automatically. On the latter, we specifically explain the methodology to map from SOAP messages to an existing structure of knowledge.
Description: The file associated with this record is embargoed until 18 months after the date of publication. The final published version may be available through the links above.
20141030T10:28:23Z

Succinct indices for range queries with applications to orthogonal range maxima
http://hdl.handle.net/2381/29206
Title: Succinct indices for range queries with applications to orthogonal range maxima
Authors: Farzan, Arash; Munro, J. Ian; Raman, Rajeev
Abstract: We consider the problem of preprocessing N points in 2D, each endowed with a priority, to answer the following queries: given a axisparallel rectangle, determine the point with the largest priority in the rectangle. Using the ideas of the effective entropy of range maxima queries and succinct indices for range maxima queries, we obtain a structure that uses O(N) words and answers the above query in O(logN loglogN) time. This a direct improvement of Chazelle's result from 1985 [10] for this problem  Chazelle required O(N/ε) words to answer queries in O((logN)[superscript 1+ε]) time for any constant ε > 0.
20141028T10:40:48Z

Succinct representations of ordinal trees
http://hdl.handle.net/2381/29205
Title: Succinct representations of ordinal trees
Authors: Raman, Rajeev; Rao, S. Srinivasa
Abstract: We survey succinct representations of ordinal, or rooted, ordered trees. Succinct representations use space that is close to the appropriate informationtheoretic minimum, but support operations on the tree rapidly, usually in O(1) time.
20141028T10:33:36Z

On probabilistic models for uncertain sequential pattern mining
http://hdl.handle.net/2381/29204
Title: On probabilistic models for uncertain sequential pattern mining
Authors: Muzammal, Muhammad; Raman, Rajeev
Editors: Cao, L.; Feng, Y.; Zhong, J.
Abstract: We study uncertainty models in sequential pattern mining. We consider situations where there is uncertainty either about a source or an event. We show that both these types of uncertainties could be modelled using probabilistic databases, and give possibleworlds semantics for both. We then describe ”interestingness” criteria based on two notions of frequentness (previously studied for frequent itemset mining) namely expected support [C. Aggarwal et al. KDD’09;Chui et al., PAKDD’07,’08] and probabilistic frequentness [Bernecker et al., KDD’09]. We study the interestingness criteria from a complexitytheoretic perspective, and show that in case of sourcelevel uncertainty, evaluating probabilistic frequentness is #Pcomplete, and thus no polynomial time algorithms are likely to exist, but evaluate the interestingness predicate in polynomial time in the remaining cases.
20141028T10:26:52Z

Encodings for range selection and topk queries
http://hdl.handle.net/2381/29203
Title: Encodings for range selection and topk queries
Authors: Grossi, Roberto; Iacono, John; Navarro, Gonzalo; Raman, Rajeev; Rao, S. Srinivasa
Abstract: We study the problem of encoding the positions the topk elements of an array A[1..n] for a given parameter 1 ≤ k ≤ n. Specifically, for any i and j, we wish create a data structure that reports the positions of the largest k elements in A[i..j] in decreasing order, without accessing A at query time. This is a natural extension of the wellknown encoding rangemaxima query problem, where only the position of the maximum in A[i..j] is sought, and finds applications in document retrieval and ranking. We give (sometimes tight) upper and lower bounds for this problem and some variants thereof.
20141028T10:16:57Z

Discovery of network properties with allshortestpaths queries
http://hdl.handle.net/2381/29198
Title: Discovery of network properties with allshortestpaths queries
Authors: Bilo, Davide; Erlebach, Thomas Rainer; Mihalak, Matus; Widmayer, Peter
Editors: Shvartsman, A. A.; Felber, P.
Abstract: We consider the problem of discovering properties (such as the diameter) of an unknown network G(V,E) with a minimum number of queries. Initially, only the vertex set V
of the network is known. Information about the edges and nonedges of the network can be obtained
by querying nodes of the network. A query at a node q∈V returns the
union of all shortest paths from q to all other nodes in V. We study the
problem as an online problem  an algorithm does not initially know the
edge set of the network, and has to decide where to make the next query
based on the information that was gathered by previous queries. We
study how many queries are needed to discover the diameter, a minimal
dominating set, a maximal independent set, the minimum degree, and
the maximum degree of the network. We also study the problem of deciding with a minimum number of queries whether the network is 2edge or
2vertex connected. We use the usual competitive analysis to evaluate the
quality of online algorithms, i.e., we compare online algorithms with optimum offline algorithms. For all properties except maximal independent
set and 2vertex connectivity we present and analyze online algorithms.
Furthermore we show, for all the aforementioned properties, that "many"
queries are needed in the worst case. As our query model delivers more
information about the network than the measurement heuristics that are
currently used in practise, these negative results suggest that a similar
behavior can be expected in realistic settings, or in more realistic models
derived from the allshortestpaths query model.
20141023T15:40:02Z

Asympotically optimal encodings for range selection
http://hdl.handle.net/2381/29193
Title: Asympotically optimal encodings for range selection
Authors: Navarro, Gonzalo; Raman, Rajeev; Satti, Srinivasa Rao
Abstract: We consider the problem of preprocessing an array A[1..n] to answer range selection and range topk queries. Given a query interval [i..j] and a value k, the former query asks for the position of the kth largest value in A[i..j], whereas the latter asks for the positions of all the k largest values in A[i..j]. We consider the encoding version of the problem, where A is not available at query time, and an upper bound kappa on k, the rank that is to be selected, is given at construction time. We obtain data structures with asymptotically optimal size and query time on a RAM model with word size Θ(lg n) : our structures use O(n lg kappa) bits and answer range selection queries in time O(1+ lg k / lg lg n) and range topk queries in time O(k), for any k ≤ kappa.
Description: The file associated with this record is embargoed until the date of the conference.
20141022T14:00:04Z

Mining statebased models from proof corpora
http://hdl.handle.net/2381/29141
Title: Mining statebased models from proof corpora
Authors: Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev
Abstract: Interactive theorem provers have been used extensively to reason about various software/hardware systems and mathematical theorems. The key challenge when using an interactive prover is finding a suitable sequence of proof steps that will lead to a successful proof requires a significant amount of human intervention. This paper presents an automated technique that takes as input examples of successful proofs and infers an Extended Finite State Machine as output. This can in turn be used to generate proofs of new conjectures. Our preliminary experiments show that the inferred models are generally accurate (contain few falsepositive sequences) and that representing existing proofs in such a way can be very useful when guiding new ones.
20141007T14:53:42Z

Dynamizing succinct tree representations
http://hdl.handle.net/2381/29103
Title: Dynamizing succinct tree representations
Authors: Joannou, Stelios; Raman, Rajeev
Abstract: We consider succinct, or spaceefficient, representations of ordinal trees. Representations exist that take 2n + o(n) bits to represent a static nnode ordinal tree  close to the informationtheoretic minimum  and support navigational operations in O(1) time on a RAM model; and some implementations have good practical performance. The situation is different for dynamic ordinal trees. Although there is theoretical work on succinct dynamic ordinal trees, there is little work on the practical performance of these data structures. Motivated by applications to representing XML documents, in this paper, we report on a preliminary study on dynamic succinct data structures. Our implementation is based on representing the tree structure as a sequence of balanced parentheses, with navigation done using the minmax tree of Sadakane and Navarro (SODA '10). Our implementation shows promising performance for update and navigation, and our findings highlight two issues that we believe will be important to future implementations: the difference between the finger model of (say) Farzan and Munro (ICALP '09) and the parenthesis model of Sadakane and Navarro, and the choice of the balanced tree used to represent the minmax tree.
20140918T08:51:47Z

A model for supporting electrical engineering with elearning
http://hdl.handle.net/2381/29066
Title: A model for supporting electrical engineering with elearning
Authors: Akaslan, Dursun
Abstract: The overall goal of this research work was developing and evaluating a model for supporting electrical engineering with elearning. The model development was based on the survey data collected from representative teachers and students in Turkey whereas the model evaluation was conducted in the relevant HEIs in Turkey and the United Kingdom. To develop the model, the study investigated the attitudes of representative key stakeholders towards elearning in Turkey by administrating questionnaires and interviews with teachers and students. Then the responses of the teachers and students were compared. Based on the results, I proposed a model with a multidimensional approach to elearning: (1) selfdirected learning by studying ebook, (2) selfassessment by solving eexercises, (3) teacherdirected learning by attending classroom sessions as an integral part of the blended learning (4) teacherassessment by solving eexercises, (5) computerdirected learning by playing egames and (6) computerassessment by solving eexercises.
To evaluate the applicability of the model in different conditions, a casecontrol study was conducted to determine whether the model had the intended effect on the participating students in HEIs in Turkey and the United Kingdom. As the result of the casecontrol study, the effects of elearning, blended learning and traditional learning were verified. However, there were significant differences among the groups. The overall scores indicated that elearning and blended learning was more effective as compared to the traditional learning. The results of our study indicated that the knowledge increase in elearners seemed to be gradual because they tended to study daily by completing each activity on time. However, the traditional learners did not have the same pattern because they usually did not read the core text and did not solve eexercise regularly before the classroom sessions. The results of preplacement, postplacement tests and middle tests also justified these assumptions.
20140908T14:27:39Z

Compressed representation of XML documents with rapid navigation
http://hdl.handle.net/2381/29062
Title: Compressed representation of XML documents with rapid navigation
Authors: Kharabsheh, Mohammad Kamel Ahmad
Abstract: XML(Extensible Markup Language) is a language used in data representation and
storage, and transmission and manipulation of data. Excessive memory consumption
is an important challenge when representing XML documents in main memory.
Document Object Model (DOM) APIs are used in a processing level that provides
access to all parts of XML documents through the navigation operations. Although
DOM serves as a a general purpose tool that can be used in different applications,
it has high memory cost particularly if using na¨ıve. The space usage of DOM has
been reduced significantly while keeping fast processing speeds, by use of succinct
data structures in SiXDOM [1]. However, SiXDOM does not explore in depth XML
data compression principles to improve inmemory space usage. Such XML data
compression techniques have been proven to be very effective in ondisk compression
of XML document. In this thesis we propose a new approach to represent XML
documents inmemory using XML data compression ideas to further reduce space
usage while rapidly supporting operations of the kind supported by DOM.
Our approach is based upon a compression method [2] which represents an XML
document as a directed acyclic graph (DAG) by sharing common subtrees. However,
this approach does not permit the representation of attributes and textual data,
and furthermore, a naive implementation of this idea gives very poor space usage
relative to other spaceefficient DOM implementations [1]. In order to realise the
potential of this compression method as an inmemory representation, a number
of optimisations are made by application of succinct data structures and variablelength
encoding. Furthermore, a framework for supporting attribute and textual
data nodes is introduced. Finally, we propose a novel approach to representing the
textual data using Minimal Perfect Hashing(MPH).
We have implemented our ideas in a software library called DAGDOMand performed
extensive experimental evaluation on a number of standard XML files. DAGDOM
yields a good result and we are able to obtain significant space reductions over existing
spaceefficient DOM implementations (typically 2 to 5 times space reduction),
with very modest degradations in CPU time for navigational operations.
20140905T15:30:29Z

Backward analysis via overapproximate abstraction and underapproximate subtraction
http://hdl.handle.net/2381/28950
Title: Backward analysis via overapproximate abstraction and underapproximate subtraction
Authors: Piterman, Nir; Bakhirkin, Alexey; Berdine, Josh
Abstract: We propose a novel approach for computing weakest liberal safe preconditions of programs. The standard approaches, which call for either underapproximation of a greatest fixed point, or complementation of a least fixed point, are often difficult to apply successfully. Our approach relies on a different decomposition of the weakest precondition of loops. We exchange the greatest fixed point for the computation of a least fixed point above a recurrent set, instead of the bottom element. Convergence is achieved using overapproximation, while in order to maintain soundness we use an underapproximating logical subtraction operation. Unlike general complementation, subtraction more easily allows for increased precision in case its arguments are related. The approach is not restricted to a specific abstract domain and we use it to analyze programs using the abstract domains of intervals and of 3valued structures.
Description: The file associated with this record is embargoed until 12 months after the date of publication. The final published version may be available through the links above.
20140626T14:09:45Z

Mining sequential patterns from probabilistic databases
http://hdl.handle.net/2381/28949
Title: Mining sequential patterns from probabilistic databases
Authors: Muzammal, Muhammad; Raman, Rajeev
Abstract: This paper considers the problem of sequential pattern mining (SPM) in
probabilistic databases. Specifically, we consider SPM in situations where there is uncertainty
in associating an event with a source, model this kind of uncertainty in the probabilistic
database framework and consider the problem of enumerating all sequences
whose expected support is sufficiently large. We give an algorithm based on dynamic
programming to compute the expected support of a sequential pattern. Next, we propose
three algorithms for mining sequential patterns from probabilistic databases. The
first two algorithms are based on the candidate generation framework – one each based
on a breadthfirst (similar to GSP) and a depthfirst (similar to SPAM) exploration
of the search space. The third one is based on the pattern growth framework (similar
to PrefixSpan). We propose optimizations that mitigate the effects of the expensive
dynamic programming computation step. We give an empirical evaluation of the probabilistic
SPM algorithms and the optimizations, and demonstrate the scalability of the
algorithms in terms of CPU time and the memory usage. We also demonstrate the
effectiveness of the probabilistic SPM framework in extracting meaningful sequences in
the presence of noise.
Description: The file associated with this record is embargoed until 12 months after the date of publication. The final published version may be available through the links above.
20140626T13:15:31Z

Designbycontract for software architectures
http://hdl.handle.net/2381/28924
Title: Designbycontract for software architectures
Authors: Poyias, Kyriakos
Abstract: We propose a design by contract (DbC) approach to specify and maintain architectural
level properties of software. Such properties are typically relevant in the design
phase of the development cycle but may also impact the execution of systems. We give a
formal framework for specifying software architectures (and their refi nements) together
with contracts that architectural con figurations abide by. In our framework, we can
specify that if an architecture guarantees a given pre condition and a refi nement rule
satisfi es a given contract, then the refi ned architecture will enjoy a given postcondition.
Methodologically, we take Architectural Design Rewriting (ADR) as our architectural
description language. ADR is a rulebased formal framework for modelling (the
evolution of) software architectures. We equip the recon figuration rules of an ADR
architecture with pre and postconditions expressed in a simple logic; a precondition
constrains the applicability of a rule while a postcondition specifi es the properties
expected of the resulting graphs. We give an algorithm to compute the weakest precondition
out of a rule and its postcondition. Furthermore, we propose a monitoring
mechanism for recording the evolution of systems after certain computations, maintaining
the history in a treelike structure. The hierarchical nature of ADR allows us to
take full advantage of the treelike structure of the monitoring mechanism. We exploit
this mechanism to formally defi ne new rewriting mechanisms for ADR reconfi guration
rules. Also, by monitoring the evolution we propose a way of identifying which part of
a system has been a ffected when unexpected runtime behaviours emerge. Moreover,
we propose a methodology that allows us to select which rules can be applied at the
architectural level to reconfigure a system so to regain its architectural style when it
becomes compromised by unexpected runtime recon figurations.
20140616T15:40:37Z

A structured approach to VO reconfigurations through Policies
http://hdl.handle.net/2381/28881
Title: A structured approach to VO reconfigurations through Policies
Authors: ReiffMarganiec, Stephan
Abstract: One of the strength of Virtual Organisations is their ability to dynamically and rapidly adapt in response
to changing environmental conditions. Dynamic adaptability has been studied in other system
areas as well and system management through policies has crystallized itself as a very prominent solution
in system and network administration. However, these areas are often concerned with very
lowlevel technical aspects. Previous work on the APPEL policy language has been aimed at dynamically
adapting system behaviour to satisfy enduser demands and – as part of STPOWLA – APPEL
was used to adapt workflow instances at runtime. In this paper we explore how the ideas of APPEL
and STPOWLA can be extended from workflows to the wider scope of Virtual Organisations. We will
use a Travel Booking VO as example.
20140530T10:52:19Z

Maintaining transactional integrity in long running workflow service : a policydriven framework
http://hdl.handle.net/2381/28880
Title: Maintaining transactional integrity in long running workflow service : a policydriven framework
Authors: ReiffMarganiec, Stephan; Ali, Manar S.
Abstract: This chapter presents a framework to provide autonomous handling of long running transactions based
on dependencies which are derived from the workflow. Business Processes naturally involve long running
activities and require transactional behaviour across them. This framework presents a solution for forward
recovery from errors by automatic application of compensation to executing instances of workflows. The
mechanism is based on propagation of failures through a recursive hierarchical structure of transaction
components (nodes and execution paths). The authors discuss a transaction management system that is
implemented as a reactive system controller, where system components change their states based on rules
in response to triggering of events, such as activation, failure, forcefail, completion, or compensation
events. One notable feature of the model is the distinction of vital and nonvital components, allowing
the process designer to express the cruciality of activities in the workflow with respect to the business
logic. Another novel feature is that in addition to dependencies arising from the structure of the workflow,
the approach also permits the workflow designer to specify additional dependencies which will also be
enforced. Thus, the authors introduce new techniques and architectures supporting enterprise integration
solutions that cater to the dynamics of business needs. The approach is implemented through workflow
actions executed by services and allows management of faults through a policydriven framework.
20140529T15:48:08Z

Encoding range minima and range top2 queries
http://hdl.handle.net/2381/28856
Title: Encoding range minima and range top2 queries
Authors: Davoodi, Pooya; Navarro, Gonzalo; Raman, Rajeev; Rao, S. Srinivasa
Abstract: We consider the problem of encoding range minimum queries (RMQs): given an array A[1..n] of distinct totally ordered values, to preprocess A and create a data structure that can answer the query RMQ(i,j), which returns the index containing the smallest element in A[i..j], without access to the array A at query time. We give a data structure whose space usage is 2n+o(n) bits, which is asymptotically optimal for worstcase data, and answers RMQs in O(1) worstcase time. This matches the previous result of Fischer and Heun, but is obtained in a more natural way. Furthermore, our result can encode the RMQs of a random array A in 1.919n+o(n) bits in expectation, which is not known to hold for Fischer and Heun’s result. We then generalize our result to the encoding range top2 query (RT2Q) problem, which is like the encoding RMQ problem except that the query RT2Q(i,j) returns the indices of both the smallest and second smallest elements of A[i..j]. We introduce a data structure using 3.272n+o(n) bits that answers RT2Qs in constant time, and also give lower bounds on the effective entropy of the RT2Q problem.
20140528T10:49:40Z

Optimal indexes for sparse bit vectors
http://hdl.handle.net/2381/28854
Title: Optimal indexes for sparse bit vectors
Authors: Golynski, Alexander; Orlandi, Alessio; Raman, Rajeev; Rao, S. Srinivasa
Abstract: We consider the problem of supporting rank and select operations on a bit vector of length m with n 1bits. The problem is considered in the succinct index model, where the bit vector is stored in "readonly" memory and an additional data structure, called the index is created during preprocessing to help answer the above queries. We give asymptotically optimal densitysensitive tradeoffs, involving both m and n, that relate the size of the index to the number of accesses to the bit vector (and processing time) needed to answer the above queries. The results are particularly interesting for the case where n=o(m).
20140527T10:19:32Z

An empirical evaluation of extendible arrays
http://hdl.handle.net/2381/28738
Title: An empirical evaluation of extendible arrays
Authors: Joannou, Stelios; Raman, Rajeev
Editors: Pardalos, PM; Rebennack, S
Abstract: We study the performance of several alternatives for implementing extendible arrays, which allow random access to elements stored
in them, whilst allowing the arrays to be grown and shrunk. The study
not only looks at the basic operations of grow/shrink and accessing data, but also the effects of memory fragmentation on performance.
Description: The final publication is
available at link.springer.com
20140409T10:40:44Z

Cellcycle regulation of NOTCH signaling during C. elegans vulval development
http://hdl.handle.net/2381/28643
Title: Cellcycle regulation of NOTCH signaling during C. elegans vulval development
Authors: NusserStein, Stefanie; Beyer, Antje; Rimann, Ivo; Adamczyk, Magdalene; Piterman, Nir; Hajnal, Alex; Fisher, Jasmin
Abstract: C. elegans vulval development is one of the best‐characterized systems to study cell fate specification during organogenesis. The detailed knowledge of the signaling pathways determining vulval precursor cell (VPC) fates permitted us to create a computational model based on the antagonistic interactions between the epidermal growth factor receptor (EGFR)/RAS/MAPK and the NOTCH pathways that specify the primary and secondary fates, respectively. A key notion of our model is called bounded asynchrony, which predicts that a limited degree of asynchrony in the progression of the VPCs is necessary to break their equivalence. While searching for a molecular mechanism underlying bounded asynchrony, we discovered that the termination of NOTCH signaling is tightly linked to cell‐cycle progression. When single VPCs were arrested in the G1 phase, intracellular NOTCH failed to be degraded, resulting in a mixed primary/secondary cell fate. Moreover, the G1 cyclins CYD‐1 and CYE‐1 stabilize NOTCH, while the G2 cyclin CYB‐3 promotes NOTCH degradation. Our findings reveal a synchronization mechanism that coordinates NOTCH signaling with cell‐cycle progression and thus permits the formation of a stable cell fate pattern.
20140307T13:50:41Z

Faster temporal reasoning for infinitestate programs
http://hdl.handle.net/2381/28591
Title: Faster temporal reasoning for infinitestate programs
Authors: Piterman, Nir; Cook, Byron; Khlaaf, Heidy
Abstract: In many model checking tools that support temporal logic, performance is hindered by redundant reasoning performed in the presence of nested temporal operators. In particular, tools supporting the statebased temporal logic CTL often symbolically partition the system's state space using the subformulae of the input temporal formula. This can lead to repeated work when tools are applied to infinitestate programs, as often the characterization of the statespaces for nearby program locations are similar and interrelated. In this paper, we describe a new symbolic procedure for CTL verification of infinitestate programs. Our procedure uses the structure of the program's controlflow graph in combination with the nesting of temporal operators in order to optimize reasoning performed during symbolic model checking. An experimental evaluation against competing tools demonstrates that our approach not only gains ordersofmagnitude performance speed improvement, but allows for scalability of temporal reasoning for larger programs.
20140220T14:08:53Z

Strongly complete logics for coalgebras
http://hdl.handle.net/2381/28587
Title: Strongly complete logics for coalgebras
Authors: Kurz, Alexander; Rosicky, Jiri
Abstract: Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for setbased coalgebras. In particular, a general construction of a logic from an arbitrary setfunctor is given and proven to be strongly complete under additional assumptions. We proceed in three parts. Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations and equations. Moreover, the presentation of the category of algebras for the functor is obtained compositionally from the presentations of the underlying category and of the functor. Part II investigates algebras for a functor over indcompletions and extends the theorem of J{'o}nsson and Tarski on canonical extensions of Boolean algebras with operators to this setting. Part III shows, based on Part I, how to associate a finitary logic to any finitesets preserving functor T. Based on Part II we prove the logic to be strongly complete under a reasonable condition on T.
20140214T10:52:40Z

Completeness for the coalgebraic cover modality
http://hdl.handle.net/2381/28586
Title: Completeness for the coalgebraic cover modality
Authors: Kupke, Clemens; Kurz, Alexander; Venema, Yde
Abstract: We study the finitary version of the coalgebraic logic introduced by L.Moss. The syntax of this logic, which is introduced uniformly with respect to a coalgebraic type functor, required to preserve weak pullbacks, extends that of classical propositional logic with a socalled coalgebraic cover modality depending on the type functor. Its semantics is defined in terms of a categorically defined relation lifting operation. As the main contributions of our paper we introduce a derivation system, and prove that it provides a sound and complete axiomatization for the collection of coalgebraically valid inequalities. Our soundness and completeness proof is algebraic, and we employ Pattinson's stratification method, showing that our derivation system can be stratified in countably many layers, corresponding to the modal depth of the formulas involved. In the proof of our main result we identify some new concepts and obtain some auxiliary results of independent interest. We survey properties of the notion of relation lifting, induced by an arbitrary but fixed set functor. We introduce a category of Boolean algebra presentations, and establish an adjunction between it and the category of Boolean algebras. Given the fact that our derivation system involves only formulas of depth one, it can be encoded as a endofunctor on Boolean algebras. We show that this functor is finitary and preserves embeddings, and we prove that the LindenbaumTarski algebra of our logic can be identified with the initial algebra for this functor.
20140214T10:40:06Z

Activity awareness in contextaware systems using software sensors
http://hdl.handle.net/2381/28379
Title: Activity awareness in contextaware systems using software sensors
Authors: Pathan, Kamran Taj
Abstract: Contextaware systems being a component of ubiquitous or pervasive computing environment sense the users’ physical and virtual surrounding to adapt their behaviour accordingly. To achieve activity context tracking devices are common practice. Service Oriented Architecture is based on collections of services that communicate with each other. The communication between users and services involves data that can be used to sense the activity context of the user. SOAP is a simple protocol to let applications exchange their information over the web. Semantic Web provides standards to express the relationship between data to allow machines to process data more intelligently.
This work proposes an approach for supporting contextaware activity sensing using software sensors. The main challenges in the work are specifying context information in a machine processable form, developing a mechanism that can understand the data extracted from exchanges of services, utilising the data extracted from these services, and the architecture that supports sensing with software sensors. To address these issues, we have provided a bridge to combine the traditional web services with the semantic web technologies, a knowledge structure that supports the activity context information in the contextaware environments and mapping methods that extract the data out of exchanges occurring between user and services and map it into a context model. The Direct Match, the Synonym Match and the Hierarchical Match methods are developed to put the extracted data from services to the knowledge structure.
This research will open doors to further develop automated and dynamic contextaware systems that can exploit the software sensors to sense the activity of the user in the contextaware environments.
20131108T15:49:07Z

Pure Type Systems with Corecursion on Streams: From Finite to Infinitary Normalisation
http://hdl.handle.net/2381/28332
Title: Pure Type Systems with Corecursion on Streams: From Finite to Infinitary Normalisation
Authors: Severi, Paula; de Vries, FerJan
Abstract: In this paper, we use types for ensuring that programs involving streams are wellbehaved.We extend pure type systems with a type constructor for streams, a modal operator next and a fixed point operator for expressing corecursion. This extension is called Pure Type Systems with Corecursion (CoPTS). The typed lambda calculus for reactive programs defined by Krishnaswami and Benton can be obtained as a CoPTS. CoPTSs allow us to study a wide range of typed lambda calculi extended with corecursion using only one framework. In particular, we study this extension for the calculus of constructions which is the underlying formal language of Coq. We use the machinery of infinitary rewriting and formalise the idea of wellbehaved programs using the concept of infinitary normalisation. The set of finite and infinite terms is defined as a metric completion. We establish a precise connection between the modal operator (• A) and the metric at a syntactic level by relating a variable of type (• A) with the depth of all its occurrences in a term. This syntactic connection between the modal operator and the depth is the key to the proofs of infinitary weak and strong normalisation.
20131028T15:24:43Z

Succinct Representations of Binary Trees for Range Minimum Queries
http://hdl.handle.net/2381/28331
Title: Succinct Representations of Binary Trees for Range Minimum Queries
Authors: Davoodi, Pooya; Raman, Rajeev; Satti, Satti Srinivasa
Abstract: We provide two succinct representations of binary trees that can be used to represent the Cartesian tree of an array A of size n. Both the representations take the optimal 2n + o(n) bits of space in the worst case and support range minimum queries (RMQs) in O(1) time. The first one is a modification of the representation of Farzan and Munro (SWAT 2008); a consequence of this result is that we can represent the Cartesian tree of a random permutation in 1.92n + o(n) bits in expectation. The second one uses a wellknown transformation between binary trees and ordinal trees, and ordinal tree operations to effect operations on the Cartesian tree. This provides an alternative, and more natural, way to view the 2DMinHeap of Fischer and Huen (SICOMP 2011). Furthermore, we show that the preprocessing needed to output the data structure can be performed in linear time using o(n) bits of extra working space, improving the result of Fischer and Heun who use n + o(n) bits working space.
20131028T13:05:12Z

Succinct representations of permutations and functions
http://hdl.handle.net/2381/28330
Title: Succinct representations of permutations and functions
Authors: Munro, J. Ian; Raman, Rajeev; Raman, Venkatesh; Rao, Satti Srinivasa
Abstract: We investigate the problem of succinctly representing an arbitrary permutation, π, on {0, . . . , n−1} so that π[superscript k](i) can be computed quickly for any i and any (positive or negative) integer power k. A representation taking (1 + ϵ)n lg n + O(1) bits suffices to compute arbitrary powers in constant time, for any positive constant ϵ ≤ 1. A representation taking the optimal ⌈lg n!⌉ + o(n) bits can be used to compute arbitrary powers in O(lg n/ lg lg n) time.
We then consider the more general problem of succinctly representing an arbitrary function, f : [n] → [n] so that f[superscript k](i) can be computed quickly for any i and any integer power k. We give a representation that takes (1 + ϵ)n lg n + O(1) bits, for any positive constant ϵ ≤ 1, and computes arbitrary positive powers in constant time. It can also be used to compute f[superscript k](i), for any negative integer k, in optimal O(1+  f[superscript k](i) ) time. We place emphasis on the redundancy, or the space beyond the informationtheoretic lower bound that the data structure uses in order to support operations efficiently. A number of lower bounds have recently been shown on the redundancy of data structures. These lower bounds confirm the space–time optimality of some of our solutions.
Furthermore, the redundancy of one of our structures "surpasses" a recent lower bound by Golynski [Golynski, SODA 2009], thus demonstrating the limitations of this lower bound.
Description: NOTICE: this is the author’s version of a work that was accepted for publication in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Theoretical Computer Science, 2012, 438, pp. 4788, DOI: 10.1016/j.tcs.2012.03.005.
20131028T12:29:09Z

Dynamic Compressed Strings with Random Access
http://hdl.handle.net/2381/28247
Title: Dynamic Compressed Strings with Random Access
Authors: Grossi, Roberto; Raman, Rajeev; Rao, Satti Srinivasa; Venturini, Rossano
Abstract: We consider the problem of storing a string S in dynamic compressed form, while permitting operations directly on the compressed representation of S: access a substring of S; replace, insert or delete a symbol in S; count how many occurrences of a given symbol appear in any given prefix of S (called rank operation) and locate the position of the ith occurrence of a symbol inside S (called select operation). We discuss the time complexity of several combinations of these operations along with the entropy space bounds of the corresponding compressed indexes. In this way, we extend or improve the bounds of previous work by Ferragina and Venturini [TCS, 2007], Jansson et al. [ICALP, 2012], and Nekrich and Navarro [SODA, 2013].
20131004T12:14:04Z