| 1. |
- Hansson, Hans
(författare)
-
ARTES - A network for Real-Time research and graduate Education in Sweden 1997-2006
- 2006
-
Bok (övrigt vetenskapligt/konstnärligt)abstract
- This book summarizes the results of the Swedish national real-time systems research initiative ARTES and provides a few representative examples of the science and scientific results that have emerged from ARTES. ARTES was supported by the Swedish Foundation for Strategic Research (SSF) with totally 95 million SEK from 1998 to 2006. ARTES has united and enforced the Swedish research community in real-time and embedded systems, and has been instrumental in advancing Sweden's international position in this area. ARTES has provided a catalytic effect and loose coordination of a total research effort many times larger than the funding provided by SSF. This has created important synergies between disciplines, enforced industrial relevance in the research, and provided important academic and industrial networking for approximately 100 senior researchers and some 200 post-graduate students.
|
|
| 2. |
- Eden, Amnon H., et al.
(författare)
-
Towards a Mathematical Foundation for Design Patterns
- 1999
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We identify a compact and sufficient set of building blocks which constitute most design patterns of the GoF catalog: uniform sets of classes or functions, function clans, class hierarchies, and regularities (morphisms) thereof. The abstractions observed are manifested within a model in symbolic logic and defined in LePUS, a declarative, higher order language. LePUS formulae concisely prescribe design patterns in a general, complete, and accurate manner. We provide a natural, condensed graphic notation for every LePUS formula and demonstrate how design patterns are faithfully portrayed by diagrams in this notation. We conclude by defining refinement (specialization) between patterns by means of predicate calculus and illustrate how the logical formalism of LePUS facilitates tool support for the recognition and implementation of design patterns.
|
|
| 3. |
- Gustavsson, Andreas, et al.
(författare)
-
Formalizing the Intent of Design Patterns. An Approach Towards a Solution to the Indexing Problem
- 1999
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The intent section of a pattern description is written in easily understood, natural language, which unfortunately has the drawback of being too imprecise and unstructured for certain applications of the intent section.We will in this essay try to formalize the intent section of a pattern description. Our aim will be to find a structure within the intent description that will reduce ambiguities and at the same time make the classification of patterns easier. The classifications of patterns addresses the problem of "labeling" patterns into one of the following categories: Creational, Structural or Behavioural. Succeeding in classifying patterns by the intent does require that enough information for doing so is contained in the one to two sentences that make up the intent. Whether this is the case or not will be discussed in the essay.A formalized intent section of a pattern description can not replace the understandability of the natural language description but can be thought of as a complement to the standard structure to patterns today.
|
|
| 4. |
- Jakobsson, Andreas, et al.
(författare)
-
Two-Dimensional Capon Spectrum Analysis
- 1999
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a computationally efficient algorithm for computing the 2-D Capon spectral estimator. The implementation is based on the fact that the 2-D data covariance matrix will have a Toeplitz-Block-Toeplitz structure, with the result that the inverse covariance matrix can be expressed in closed form by using a special case of the Gohberg-Heinig formula that is a function of strictly the forward 2-D prediction matrix polynomials. Furthermore, we present a novel method, based on a 2-D lattice algorithm, to compute the needed forward prediction matrix polynomials and discuss the difference in the so-obtained 2-D spectral estimate as compared to the one obtained by using the prediction matrix polynomials given by the Whittle-Wiggins-Robinson algorithm. Numerical simulations illustrate the clear computational gain in comparison to both the well-known classical implementation and the method recently published by Liu et al.
|
|
| 5. |
- Jansson, Anders, et al.
(författare)
-
Trafiksäkerhet och informationsmiljö i tågförarsystemet. Litteraturöversikt och olycksfallsanalyser
- 1999
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This literature survey focuses on studies of the train driver system and its connections to other parts of the larger train traffic system. The main part of the studies concern Swedish conditions, but other references are included as well.In the first part, different ways of analysing accidents are discussed, including organisational aspects. In the second part, research results from different areas, all assumed to be relevant to the train driver task, are aggregated into a body of knowledge about the train driver system. Comparisons are made between the train driver task and other operator tasks. Further, the effects of a higher degree of automation are discussed.The task of driving a train is modelled as a dynamic decision task, where the driver's mental representation of the technical system and the optic flow of information are assumed to be important parts of the train driver task.In the last part of the literature survey, the content of 40 accident reports is discussed. Further, an analysis and a classification of Swedish train accidents are made by using CREAM (Hollnagel, 1998). The content of the reports, as well as the CREAM-method are evaluated, and different classification criteria are discussed.
|
|
| 6. |
- Lin, Huimin, et al.
(författare)
-
A Proof System for Timed Automata
- 1999
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- A proof system for timed automata is presented, based on a CCS-style language for describing timed automata. It consists of the standard monoid laws for bisimulation and a set of inference rules. The judgements of the proof system are \emphconditional equations of the form \phi\rhd t=u where ϕ is a clock constraint and t, u are terms denoting timed automata. It is proved that the proof system is complete over the recursion-free subset of the language. The completeness proof relies on the notion of \emphsymbolic timed bisimulation. Two variations of the axiomatisation are also discussed, one on timed automata by associating an invariant constraint to each node and the other on bisimulation by abstracting away delay transitions.
|
|
| 7. |
- Lundqvist, Kristina, et al.
(författare)
-
A Formal Model of a Ravenscar-Compliant Run-Time Kernel and Application Code
- 1999
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The Ravenscar tasking profile for Ada95 has been designed to allow implementation of safety critical systems in Ada. Ravenscar defines a tasking run-time system with deterministic behaviour and low complexity. We provide a formal model of the primitives provided by Ravenscar. This formal model can be used to verify safety properties of applications targeting a Ravenscar-compliant run-time system. As an illustration of this, we model a sample application and formally verify its correctness using the real-time model checker UPPAAL.
|
|
| 8. |
- Söderström, Torsten, et al.
(författare)
-
Parameter Estimation for Diffusion Models
- 1999
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In many applications, for example in heat diffusion and in flow problems, it is important to describe the process behavior inside the particular medium. An example can be the strive for estimating certain parameters related to the material. This paper describes how the diffusion, modeled by a partial differential equation, can be solved using numerical methods and how results from the field of system identification can be utilized in order to estimate the parameters of interest.
|
|
| 9. |
- Brus, Linda
(författare)
-
Nonlinear identification of a solar heating system
- 2005
-
Ingår i: Proceedings of the 2005 IEEE International Conference on Control Application. - : Dept. of Information Technology. - 0780393546 ; , s. 1491-1497
-
Konferensbidrag (refereegranskat)abstract
- The use of solar heating systems is a way of exploiting the clean and free energy from the sun. To optimize the energy gain from such a system, where the main input, the solar insolation, is an uncontrollable variable, good models of the system dynamics are required. Identification methods are often either highly specialized for the application or require an extensive amount of data, especially when the dynamics studied are nonlinear. This paper shows that by application of a new recursive system identification technique, a small scale solar heating system can be modeled with very little data, without having to tailor the model structure to the application.
|
|
| 10. |
- Brus, Linda
(författare)
-
Nonlinear identification of an anaerobic digestion process
- 2005
-
Ingår i: Proceedings of the 2005 IEEE International Conference on Control Applications. - : Dept. of Information Technology. - 0780393546 ; , s. 137-142
-
Konferensbidrag (refereegranskat)abstract
- Anaerobic digestion in bioreactors is an important technology for environmental friendly treatment of organic waste. To optimize and control such processes accurate dynamic models of the process are needed. Unfortunately, modeling of anaerobic digestion often results in high order nonlinear models with many unknown parameters, a fact that complicates controller design. This paper attempts to circumvent this problem, by application of new recursive system identification techniques, thereby radically reducing the degree of the models and the number of parameters. Experiments show that a second order nonlinear model is sufficient for accurate modeling of the system.
|
|
| 11. |
- Hessel, Anders, et al.
(författare)
-
Model-based Testing of a WAP Gateway: an Industrial Case-Study
- 2006
-
Ingår i: Lecture Notes in Computer Science, vol. 4346. - : Uppsala Universitet, Uppsala. - 3540709517 ; , s. 116-131
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present experiences from a case study where a model-based approach to black-box testing is applied to verify that a Wireless Application Protocol (WAP) gateway conforms to its specification.The WAP gateway is developed by Ericsson and used in mobile telephone networks to connect mobile phones with the Internet. We focus on testing the software implementing the session (WSP) and transaction (WTP) layers of the WAP protocol. These layers, and their surrounding environment, are described as a network of timed automata. To model the many sequence numbers (from a large domain) used in the protocol, we introduce an abstraction technique. We believe the suggested abstractiontechnique will prove useful to model and analyse other similar protocols with sequence numbers, in particular in the context of model-based testing.A complete test bed is presented, which includes generation and execution of test cases. It takes as input a model and a coverage criterion expressed as an observer, and returns a verdict for each test case. The test bed includes existingtools from Ericsson for test-case execution. To generate test suites, we use our own tool CoVer --- a new test-case generation tool based on the real-time model-checker Uppaal.
|
|
| 12. |
|
|
| 13. |
- Kauppi, Arvid, et al.
(författare)
-
Control strategies for managing train traffic : Difficulties today and visions for the future
- 2006
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In 1996, on initiative from the Swedish National Rail Administration, the department of Human-Computer Interaction at the institute for Information Technology, Uppsala University initiated a research project with the objective to identify the difficulties present in today's train traffic control today and to find solutions to those problems, if possible.This paper describes the strategy used to control train traffic in Sweden today. Problems and difficulties inherited from the use of the current control strategies and systems are presented. With the goal to solve these problems, and aid the human operator in their work, solutions for new principles for control and a new control strategy are proposed - control by re-planning. The proposed control strategy is designed to support the train dispatcher to work in a more preventive manner and thereby avoiding potential disturbances in traffic when possible. The focus of control tasks will be shifted from controlling infrastructure on a technical level to focus more on a higher level of controlling the traffic flow through re-planning tasks. The new control strategy in combination with a new approach to automation, higher availability of decision relevant information and new graphical user interfaces addresses many of the issues and problems found in the control environment today.
|
|
| 14. |
- Wikström, Johan, et al.
(författare)
-
Designing a graphical user interface for train traffic control
- 2006
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In 1996, on initiative of the Swedish National Rail Administration, a research study was initiated by the department of Human Computer Interaction at Uppsala University with the aim to learn more about the problems and difficulties involved in train traffic control. As a result of this study, and the developing situation with higher speeds, more frequent traffic, and many competing train traffic operators, a research project was initiated. The purpose was to find new strategies and technical solutions for future train traffic control.Modern research on human-computer interaction in complex and dynamic systems provided a framework for how to design an interface meeting these demands. Important aspects concern e.g. workload, situation awareness and automated cognitive processes, limitations in human memory capacity, cognitive work environment problems, human error performance and dynamic decision processes. Throughout the research a user centered approach has been applied. The new proposed interface is designed to integrate all decision relevant information into one unified interface and to support a continuous awareness of the dynamic development of the traffic process. A prototype of new train traffic control interface has been implemented in close collaboration with active train dispatchers. Early and promising in-house tests have been made using the prototype described in this paper. More extensive case studies and experiments need to be conducted before a complete evaluation can be made.
|
|
| 15. |
- Nordström, Erik, et al.
(författare)
-
A Cross-Environment Study of Routing Protocols for Wireless Multi-hop Networks
- 2007
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We study ad hoc routing protocol mechanisms that impact the performance during and after periods of connectivity change. Our evaluation procedure is facilitated by using a structured and tool-supported approach, combining real world experiments with simulation and emulation. This method enables us to find performance-critical time regions in our traces. Our analysis shows that performance is largely determined by how accurately a protocol senses connectivity in these regions. Inaccurate sensing can seriously affect the performance of the protocol, even after the critical regions. We identify three significant problems with sensing that we call Self-interference, TCP backlashing and Link cache poisoning. We discuss their effect on the design of sensing mechanisms in routing protocols and suggest how the protocols can be made more robust.
|
|
| 16. |
- Saksena, Mayank, et al.
(författare)
-
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols : (Extended Version)
- 2007
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a technique for modeling and automatic verification of network protocols, based on graph transformation. It is suitable for protocols with a potentially unbounded number of nodes, in which the structure and topology of the network is a central aspect, such as routing protocols for ad hoc networks. Safety properties are specified as a set of undesirable global configurations. We verify that there is no undesirable configuration which is reachable from an initial configuration, by means of symbolic backward reachability analysis.In general, the reachability problem is undecidable. We implement the technique in a graph grammar analysis tool, and automatically verify several interesting nontrivial examples. Notably, we prove loop freedom for the DYMO ad hoc routing protocol. DYMO is currently on the IETF standards track, to potentially become an Internet standard.
|
|
| 17. |
|
|
| 18. |
|
|
| 19. |
- Abbas, Qaisar, et al.
(författare)
-
A weak boundary procedure for high order finite difference approximations of hyperbolic problems
- 2011
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We introduce a new weak boundary procedures for high order finite difference operators on summation-by-parts type applied to hyperbolic problems. The boundary procedure is applied in an extended domain where data is known. We show how to raise the order of accuracy for a diagonal norm based approximation and how to modify the spectrum of the resulting operator to get a faster convergence to steady-state. Furthermore, we also show how to construct better non-reflecting properties at the boundaries using the above procedure. Numerical results that corroborate the analysis are presented.
|
|
| 20. |
- Abd-Elrady, Emad
(författare)
-
An adaptive grid point RPEM algorithm for harmonic signal modeling
- 2001
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Periodic signals can be modeled as a real wave with unknown period in cascade with a piecewise linear function. In this report, a recursive Gauss-Newton prediction error identification algorithm for joint estimation of the driving frequency and the parameters of the nonlinear output function parameterized in a number of adaptively estimated grid points is introduced. The Cramer-Rao bound (CRB) is derived for the suggested algorithm. Numerical examples indicate that the suggested algorithm gives better performance than using fixed grid point algorithms and easily can be modified to track both the fundamental frequency variations and the time varying amplitude.
|
|
| 21. |
- Abd-Elrady, Emad, et al.
(författare)
-
Bias Analysis in Least Squares Estimation of Periodic Signals Using Nonlinear ODE's
- 2004
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Periodic signals can be modeled by means of second-order nonlinear ordinary differential equations (ODE's). The right hand side function of the ODE is parameterized in terms of known basis functions. The least squares algorithm developed for estimating the coefficients of these basis functions gives biased estimates, especially at low signal to noise ratios. This is due to noise contributions to the periodic signal and its derivatives evaluated using finite difference approximations. In this paper an analysis for this bias is given.
|
|
| 22. |
- Abd-Elrady, Emad
(författare)
-
Convergence of the RPEM as applied to harmonic signal modeling
- 2000
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Arbitrary periodic signals can be estimated recursively by exploiting the fact that a sine wave passing through a static nonlinear function generates a spectrum of overtones. The estimated signal model is hence parameterized as a real wave with unknown period in cascade with a piecewise linear function. The driving periodic wave can be chosen depending on any prior knowledge. The performance of a recursive Gauss-Newton prediction error identification algorithm for joint estimation of the driving frequency and the parameters of the nonlinear output function is therefore studied. A theoretical analysis of local convergence to the true parameter vector as well as numerical examples are given. Furthermore, the Cramer-Rao bound (CRB) is calculated in this report.
|
|
| 23. |
|
|
| 24. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Algorithmic Improvements in Regular Model Checking
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems, whose states can be represented as finite strings of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. In earlier papers, we have developed methods for computing the transitive closure (or the set of reachable states) of the transition relation, represented by a regular length-preserving transducer. In this paper, we present several improvements of these techniques, which reduce the size of intermediate approximations of the transitive closure: One improvement is to pre-process the transducer by \em bi-determinization, another is to use a more powerful equivalence relation for identifying histories (columns) of states in the transitive closure. We also present a simplified theoretical framework for showing soundness of the optimization, which is based on commuting simulations. The techniques have been implemented, and we report the speedups obtained from the respective optimizations.
|
|
| 25. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Better-Structured Transition Systems
- 2004
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In automated verification of infinite-state systems, a variety of algorithms that operate on constraints representing sets of states have been developed. Many of these algorithms rely on well quasi-ordering of the constraint system for proving termination. A number of methods for generating new well quasi-ordered constraint systems have been proposed. However, many of these constraint systems suffer from constraint explosion as the number of constraints generated during analysis grows exponentially with the size of the problem. We suggest using the theory of better quasi-ordering to prove termination since that will allow generation of constraint systems that are less prone to constraint explosion. We also present a method to derive such constraint systems. We introduce existential zones, a constraint system for verification of systems with an unbounded number of clocks and use our methodology to prove that existential zones are better quasi-ordered. We show how to use existential zones in verification of timed Petri nets and present some experimental results. Finally, we present several other constraint systems which have been derived using our methodology.
|
|
| 26. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
BQOs and Timed Petri Nets
- 2000
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In this paper, we use the theory of better quasi-orderings to define a methodology for inventing constraint systems which are both well quasi-ordered and compact. We apply our methodology by presenting new constraint systems for verification of systems with unboundedly many real-valued clocks, and use them for checking safety properties for lazy (non-urgent) timed Petri nets where each token is equipped with a real-valued clock.
|
|
| 27. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Downward Closed Language Generators
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We use downward closed languages for representing sets of states when performing forward reachability analysis on infinite-state systems. Downward closed languages are often more succinct than exact representations of the set of reachable states. We introduce a formalism for representing downward closed languages, called downward closed language generators (dlgs). We show that standard set operations needed for performing symbolic reachability analysis are computable for dlgs. Using a class of hierarchically defined dlgs, we have implemented a prototype for analysing timed Petri nets and used it to analyze a parameterized version of Fischer's protocol. We also show how dlgs can be used for uniform representation of formalisms previously presented for models such as Petri nets and lossy channel systems.
|
|
| 28. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Eager Markov Chains
- 2006
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider infinite-state discrete Markov chains which are \empheager: the probability of avoiding a defined set of final states for more than n steps decreases exponentially in n. We study the problem of computing the expected reward (or cost) of runs until reaching the final states, where rewards are assigned to individual runs by computable reward functions. We present a path exploration scheme, based on forward reachability analysis, to approximate the expected reward up-to an arbitrarily small error, and show that the scheme is guaranteed to terminate in the case of eager Markov chains. We show that eager Markov chains include those induced by Probabilistic Vector Addition Systems with States, Noisy Turing Machines, and Probabilistic Lossy Channel Systems.
|
|
| 29. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Forward Reachability Analysis of Timed Petri Nets
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider verification of safety properties for concurrent real-timed systems modelled by timed Petri nets, by performing symbolic forward reachability analysis. We introduce a formalism, called region generators for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions. Downward closed languages provide exact abstractions of sets of reachable states with respect to safety properties.We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples.We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer's protocol. We also used the tool to generate a finite-state abstraction of the protocol.
|
|
| 30. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Limiting Behavior of Markov Chains with Eager Attractors
- 2006
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider discrete infinite-state Markov chains which contain an eager finite attractor. A finite attractor is a finite subset of states that is eventually reached with probability 1 from every other state, and the eagerness condition requires that the probability of avoiding the attractor in n or more steps after leaving it is exponentially bounded in n. Examples of such Markov chains are those induced by probabilistic lossy channel systems and similar systems. We show that the expected residence time (a generalization of the steady state distribution) exists for Markov chains with eager attractors and that it can be effectively approximated to arbitrary precision. Furthermore, arbitrarily close approximations of the limiting average expected reward, with respect to state-based bounded reward functions, are also computable.
|
|
| 31. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Multi-Clock Timed Networks
- 2004
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider verification of safety properties for parameterized systems of timed processes, so called ıt timed networks. A timed network consists of a finite state process, called a controller, and an arbitrary set of identical timed processes. In a previous work, we showed that checking safety properties is decidable in the case where each timed process is equipped with a single real-valued clock. It was left open whether the result could be extended to multi-clock timed networks. We show that the problem becomes undecidable when each timed process has two clocks. On the other hand, we show that the problem is decidable when clocks range over a discrete time domain. This decidability result holds when processes have any finite number of clocks.
|
|
| 32. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
R-automata
- 2008
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We introduce \emphR-automata – a model for analysis of systems with resources which are consumed in small parts but which can be replenished at once. An R-automaton is a finite state machine which operates on a finite number of unbounded counters (modeling the resources). The values of the counters can be incremented, reset to zero, or left unchanged along the transitions. We define the language accepted by an R-automaton relative to a natural number D as the set of words allowing a run along which no counter value exceeds D. As the main result, we show decidability of the universality problem, i.e., the problem whether there is a number D such that the corresponding language is universal. The decidability proof is based on a reformulation of the problem in the language of finite monoids and solving it using the factorization forest theorem. This approach extends the way in which the factorization forest theorem was used to solve the limitedness problem for distance automata in Simon, 1994. We also show decidability of the non-emptiness problem and the limitedness problem, i.e., whether there is a natural number D such that the corresponding language is non-empty resp.\ all the accepted words can also be accepted with counter values smaller than D. Finally, we extend the decidability results to R-automata with Büchi acceptance conditions.
|
|
| 33. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems)
- 2006
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We give a simple and efficient method to prove safety properties for parameterized systems with linear topologies. A process in the system is a finite-state automaton, where the transitions are guarded by both local and global conditions. Processes may communicate via broadcast, rendez-vous and shared variables. The method derives an over-approximation of the induced transition system, which allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency. We have implemented a prototype which works well on several mutual exclusion algorithms and cache coherence protocols.
|
|
| 34. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stochastic Games with Lossy Channels
- 2007
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider turn-based stochastic games on infinite graphs induced by game probabilistic lossy channel systems (GPLCS), the game version of probabilistic lossy channel systems (PLCS). We study games with Buchi (repeated reachability) objectives and almost-sure winning condition. Under the assumption that the target set is regular, a symbolic representation of the set of winning states for each player can be effectively constructed. Thus, turn-based stochastic games on GPLCS are decidable. This generalizes earlier decidability result for PLCS-induced Markov decision processes. Our scheme can be adapted to GPLCS with simple reachability objectives.
|
|
| 35. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Timed Lossy Channel Systems
- 2012
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Lossy channel systems are a classical model with applications ranging from the modeling of communication protocols to programs running on weak memory models. All existing work assume that messages traveling inside the channels are picked from a finite alphabet. In this paper, we extend the model by assuming that each message is equipped with a clock representing the age of the message, thus obtaining the model of \emphTimed Lossy Channel Systems (TLCS). The main contribution of the paper is to show that the control state reachability problem is decidable for TLCS.
|
|
| 36. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Verification of Probabilistic Systems with Faulty Communication
- 2002
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Many protocols are designed to operate correctly even in the case where the underlying communication medium is faulty. To capture the behaviour of such protocols, lossy channel systems (LCS) \citeAbJo:lossy:IC have been proposed. In an LCS the communication channels are modelled as FIFO buffers which are unbounded, but also unreliable in the sense that they can nondeterministically lose messages. Recently, several attempts \citeBaEn:plcs,ABIJ:problossy have been made to study probabilistic Lossy Channel Systems (PLCS) in which the probability of losing messages is taken into account. In this paper, we consider a variant of PLCS which is more realistic than those studied in \citeBaEn:plcs,ABIJ:problossy. More precisely, we assume that during each step in the execution of the system, each message may be lost with a certain predefined probability. We show that for such systems the following model checking problem is decidable: to verify whether a given property definable by finite state ømega-automata holds with probability one. We also consider other types of faulty behavior, such as corruption and duplication of messages, and insertion of new messages, and show that the decidability results extend to these models.
|
|
| 37. |
- Abdulla, Parosh, et al.
(författare)
-
Closed, Open and Robust Timed Networks
- 2004
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider verification of safety properties for parameterized systems of timed processes, so called 'timed networks'. A timed network consists of a finite state process, called a controller, and an arbitrary set of identical timed processes. In [AJ03] it was shown that checking safety properties is decidable in the case where each timed process is equipped with a single real-valued clock. In [ADM04], we showed that this is no longer possible if each timed process is equipped with at least two real-valued clocks. In this paper, we study two subclasses of timed networks: 'closed' and 'open' timed networks. In closed timed networks, all clock constraints are non-strict, while in open timed networks, all clock constraints are strict (thus corresponds to syntactic removal of equality testing). We show that the problem becomes decidable for closed timed network, while it remains undecidable for open timed networks. We also consider 'robust' semantics of timed networks by introducing timing fuzziness through semantic removal of equality testing. We show that the problem is undecidable both for closed and open timed networks under the robust semantics.
|
|
| 38. |
- Abdulla, Parosh, et al.
(författare)
-
Decidability of Zenoness, Token Liveness and Boundedness of Dense-Timed Petri Nets
- 2004
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider 'Timed Petri Nets (TPNs)' : extensions of Petri nets in which each token is equipped with a real-valued clock. We consider the following three verification problems for TPN. (i) 'Zenoness:' whether there is an infinite computation from a given marking which takes only a finite amount of time. We show decidability of zenoness for TPNs, thus solving an open problem from \citeEscrig:etal:TPN. (ii) 'Token liveness:' whether a token is ıt alive in a marking, i.e., whether there is a computation from the marking which eventually consumes the token. We show decidability of the problem by reducing it to the 'coverability problem', which is decidable for TPNs. (iii) 'Boundedness:' whether the size of the reachable markings is bounded. We consider two versions of the problem; namely 'semantic boundedness' where only live tokens are taken into consideration in the markings, and 'syntactic boundedness' where also dead tokens are considered. We show undecidability of semantic boundedness, while we prove that syntactic boundedness is decidable through an extension of the Karp-Miller algorithm.
|
|
| 39. |
- Abdulla, Parosh, et al.
(författare)
-
Handling Parameterized Systems with Non-Atomic Global Conditions
- 2007
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider verification of safety properties for parameterized systems with linear topologies. A process in the system is an extended automaton, where the transitions are guarded by both local and global conditions. The global conditions are non-atomic, i.e., a process allows arbitrary interleavings with other transitions while checking the states of all (or some) of the other processes. We translate the problem into model checking of infinite transition systems where each configuration is a labeled finite graph. We derive an over-approximation of the induced transition system, which leads to a symbolic scheme for analyzing safety properties. We have implemented a prototype and run it on several nontrivial case studies, namely non-atomic versions of Burn's protocol, Dijkstra's protocol, the Bakery algorithm, Lamport's distributed mutual exclusion protocol, and a two-phase commit protocol used for handling transactions in distributed systems. As far as we know, these protocols have not previously been verified in a fully automated framework.
|
|
| 40. |
- Adams, Robin, et al.
(författare)
-
What is the word for 'Engineering' in Swedish : Swedish students conceptions of their discipline
- 2007
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Engineering education in Sweden – as in the rest of the world – is experiencing a decline in student interest. There are concerns about the ways in which students think about engineering education, why they join an academic programme in engineering, and why they persist in their studies. In this context the aims of the Nationellt ämnesdidaktiskt Centrum för Teknikutbildning i Studenternas Sammanhang project (CeTUSS) is to investigate the student experience and to identify and support a continuing network of interested researchers, as well as in building capacity for disciplinary pedagogic investigation. The Stepping Stones project brings together these interests in a multi-researcher, multi-institutional study that investigates how tudents and academic staff perceive engineering in Sweden and in Swedish education. The first results of that project are reported here. As this study is situated uniquely in Swedish education, it allows for exploration of “a Swedish perspective” on conceptions of engineering. The Stepping Stones project was based on a model of research capacity-building previously instantiated in the USA and Australia (Fincher & Tenenberg, 2006).
|
|
| 41. |
|
|
| 42. |
|
|
| 43. |
- Alves, Ricardo, et al.
(författare)
-
Minimizing Replay under Way-Prediction
- 2019
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Way-predictors are effective at reducing dynamic cache energy by reducing the number of ways accessed, but introduce additional latency for incorrect way-predictions. While previous work has studied the impact of the increased latency for incorrect way-predictions, we show that the latency variability has a far greater effect as it forces replay of in-flight instructions on an incorrect way-prediction. To address the problem, we propose a solution that learns the confidence of the way-prediction and dynamically disables it when it is likely to mispredict. We further improve this approach by biasing the confidence to reduce latency variability further at the cost of reduced way-predictions. Our results show that instruction replay in a way-predictor reduces IPC by 6.9% due to 10% of the instructions being replayed. Our confidence-based way-predictor degrades IPC by only 2.9% by replaying just 3.4% of the instructions, reducing way-predictor cache energy overhead (compared to serial access cache) from 8.5% to 1.9%.
|
|
| 44. |
- Amnell, Tobias, et al.
(författare)
-
Code Synthesis for Timed Automata
- 2002
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a framework for development of real-time embedded systems based on the recently presented model of timed automata extended with real-time tasks. It has been shown previously that design problems such as reachability and schedulability are decidable for the model of timed automata with tasks. In this paper we describe how to automatically synthesise executable code with predictable timing behaviour, which is guaranteed to meet constraints (timing and other) imposed on the design model. To demonstrate the applicability of the framework, implemented in the Times tool, we present a case-study of a well known production cell, built in LEGO and controlled by a Hitachi H8 based LEGO Mindstorm control brick.
|
|
| 45. |
- Andersson, Arne, et al.
(författare)
-
A New Analysis of Combinatorial vs Simultaneous Auctions: Revenue and Efficiency
- 2008
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We address the fundamental issue of revenue and efficiency in the combinatorial and simultaneous auction using a novel approach. Specifically, upper and lower bounds are constructed for the first-price sealed-bid setting of these two auctions. The question of revenue is important yet very few results can be found in the literature. Only for very small instances with 2 items have comparisons been made. Krishna et. al. find that allowing combinatorial bids result in lower revenue compared to a second price simultaneous auction. We formulate a lower bound on the first-price combinatorial auction and an upper bound on the first-price simultaneous auction for larger problems with several items and many bidders, in a model where bidders have synergies from winning a specific set of items. We show that the combinatorial auction is revenue superior to the simultaneous auction for a specific instance in pure symmetric equilibrium and give two generalized upper bounds on revenue for the simultaneous auction.
|
|
| 46. |
- Andersson, Arne, et al.
(författare)
-
A New Analysis of Revenue in the Combinatorial and Simultaneous Auction
- 2009
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We prove that in many cases, a first-price sealed-bid combinatorial auction gives higher expected revenue than a sealed-bid simultaneous auction. This is the first theoretical evidence that combinatorial auctions indeed generate higher revenue, which has been a common belief for decades.We use a model with many bidders and items, where bidders are of two types: (i) single-bidders interested in only one item and (ii) synergy-bidders, each interested in one random combination of items. We provide an upper bound on the expected revenue for simultaneous auctions and a lower bound on combinatorial auctions. Our bounds are parameterized on the number of bidders and items, combination size, and synergy.We derive an asymptotic result, proving that as the number of bidders approach infinity, expected revenue of the combinatorial auction will be higher than that of the simultaneous auction. We also provide concrete examples where the combinatorial auction is revenue-superior.
|
|
| 47. |
- Andersson, Arne, et al.
(författare)
-
Integer Programming for Automated Auctions
- 1999
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Auctions allowing bids for combinations of items are important for (agent mediated) electronic commerce; compared to other auction mechanisms, they often increase the efficiency of the auction, while keeping risks for bidders low. The determination of an optimal winner combination in this type of auctions is a complex computational problem, which has recently attracted some research, and in this paper, we look further into the topic.It is well known that the winner determination problem for a certain class of auctions is equivalent to what in the operations research community is referred to as (weighted) set packing. In this paper we compare some of the recent winner determination algorithms to traditional set packing algorithms, and study how more general auctions can be modeled by use of standard integer programming methods.Note: Final version published at ICMAS-00 available from http://www.csd.uu.se/~arnea/abs/icmas00.html
|
|
| 48. |
- Andersson, Arne, et al.
(författare)
-
Managing Large Scale Computational Markets
- 2000
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- General equilibrium theory has been proposed for resource allocation in computational markets. The basic procedure is that agents submit bids and that a resource (re)allocation is performed when a set of prices (one for each commodity) is found such that supply meets demand for each commodity. For successful implementation of large markets based on general equilibrium theory, efficient algorithms for finding the equilibrium are required. We discuss some drawbacks of current algorithms for large scale equilibrium markets and present a novel distributed algorithm, CoTree, which deals with the most important problems. CoTree is communication sparse, fast in adapting to preference changes of a few agents, have minimal requirements on local data, and is easy to implement.
|
|
| 49. |
- Andersson, Arne, et al.
(författare)
-
Resource Allocation With Noisy Functions
- 2000
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider resource allocation with separable objective functions defined over subranges of the integers. While it is well known that (the maximisation version of) this problem can be solved efficiently if the objective functions are concave, the general problem of resource allocation with functions that are not necessarily concave is difficult. In this article we show that for a large class of problem instances with noisy objective functions the optimal solutions can be computed efficiently. We support our claims by experimental evidence. Our experiments show that our algorithm in hard and practically relevant cases runs up to 40 - 60 times faster than the brute force testing of all possible solutions.
|
|
| 50. |
- Andreasson, Mattias, et al.
(författare)
-
Project Avatar Developing a Distributed Mobile Phone Game
- 2006
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Team Avatar, as the members of Project Avatar have come to be known by, is a group of 4th year computer science students at Uppsala University that have been developing a distributed mobile phone game during the fall of 2005. In this paper we describe the general design and environment of the result of Project Avatar - the game Three Crowns.
|
|
