2007 - Technical Reports
Number Report Title 2007/1 A GENERIC ALGORITHM FOR AUTOMATED MODEL FORMULATION
Obinna Ezechukwu, Istvan Maros, 33pp
2007/2 RCAT: FROM PEPA TO PRODUCT FORM
Jeremy T. Bradley, 8pp
2007/3 A MULTIOBJECTIVE DYNAMIC NONLINEAR ROBOT ASSIGNMENT PROBLEM
Sampo Ruuth, Istvan Maros, Kimmo Nieminen , 15pp
2007/4 PSPACE BOUNDS FOR RANK-1 MODAL LOGICS
Dirk Pattinson, Lutz Schroeder , 30pp
2007/5 MULTIPARTY ASYNCHRONOUS SESSION TYPES
Kohei Honda, Nobuko Yoshida, and Marco Carbone, 75pp
Obinna Ezechukwu, Istvan Maros, 33ppReport: 2007/1
The challenge of automating the formulation of optimization models is to produce, from a problem description, a well-formed model, which is a mathematically accurate representation of the real-world decision-making problem being considered, and which is suitable for computational purposes. This can be stated more formally as the automation problem, which is the problem of providing intelligent (i.e. automated) assistance during the formulation stage of the mathematical programming process. In this paper, we explore the need to automate model formulation, thus providing a background on the automation problem. We also detail a solution to the problem which is based on evolutionary search techniques.
Jeremy T. Bradley, 8ppReport: 2007/2
A short introduction to RCAT and reversed processes based on the stochastic process algebra PEPA. We make use of the standard PEPA syntax throughout and show how product form steady state formulae can be produced using RCAT. This is used on the Performance Analysis course (336) in the Department of Computing. .
Sampo Ruuth, Istvan Maros, Kimmo Nieminen , 15ppReport: 2007/3
Robots will be used under rapidly changing and highly dangerous circumstances such as rescue operations in a radioactive environment or a fire as well as military operations. The robots are sent to several targets in order to carry out various tasks. The robots we are considering here are able to send and receive messages to and from each other as well as solve nonlinear assignment problems. When the robot salvo is en-route to their targets several events may happen. A number of co-operative robots may get jammed as a consequence of disturbances. Some robots may already have reached their targets. Some robots may not be able to reach all targets. The system being investigated enables the surviving robots to work together in real time and change their pre-set tasks if necessary in order to maximize their effectiveness. In this paper we present a method which solves the reallocation problem using a piecewise linear network algorithm. Experimental results up to 493 targets and 500 robots show that the reallocation of the robots can be done in real time. .
Dirk Pattinson, Lutz Schroeder , 30ppReport: 2007/4
For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatisation, in PSPACE. This leads to a unified derivation of tight PSPACE-bounds for a number of logics including K, KD, coalition logic, graded modal logic, majority logic, and probabilistic modal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.
Kohei Honda, Nobuko Yoshida, and Marco Carbone, 75ppReport: 2007/5
Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-based programming, session types have been studied over the last decade for a wide range of process calculi and programming languages, focussing on binary (two-party) sessions. This work extends the foregoing theories of binary session types to multiparty, asynchronous sessions, which often arise in practical communication-centred applications. Presented as a typed calculus for mobile processes, the theory introduces a new notion of types in which interactions involving multiple peers are directly abstracted as a global scenario. Global types retain a friendly type syntax of binary session types while capturing complex causal chains of multiparty asynchronous interactions. A global type plays the role of a shared agreement among communication peers, and is used as a basis of efficient type checking through its projection onto individual peers. The fundamental properties of the session type discipline such as communication safety and progress are established for general n-party asynchronous interactions.