25 research outputs found
Complexity in Simplicity: Flexible Agent-based State Space Exploration
No full textIn this paper, we describe a new flexible framework for state space exploration based on cooperating agents. The idea is to let various agents with different search patterns explore the state space individually and communicate information about fruitful subpaths of the search tree to each other. That way very complex global search behavior is achieved with very simple local behavior. As an example agent behavior, we propose a novel anytime randomized search strategy called frustration search. The effectiveness of the framework is illustrated in the setting of priced timed automata on a number of case studies
Optimal Conditional Reachability for Multi-Priced Timed Automata
No full textIn this paper, we prove decidability of the optimal conditional reachability problem for multi-priced timed automata, an extension of timed automata with multiple cost variables evolving according to given rates for each location. More precisely, we consider the problem of determining the minimal cost of reaching a given target state, with respect to some primary cost variable, while respecting upper bound constraints on the remaining (secondary) cost variables. Decidability is proven by constructing a zone-based algorithm that always terminates while synthesizing the optimal cost with a single secondary cost variable. The approach is then lifted to any number of secondary cost variables
On using priced timed automata to achieve optimal scheduling
No full textThis contribution reports on the considerable effort made recentlytowards extending and applying well-established timedautomata technology to optimal scheduling and planningproblems. The effort of the authors in this direction has to alarge extent been carried out as part of the European projectsVHS (VHS 2005) and AMETIST (AMETIST 2005) and areavailable in the recently released UPPAAL CORA (UPPAALCORA 2005), a variant of the real-time verification tool UPPAAL(Larsen, Pettersson, & Yi 1997; Behrmann, David, &Larsen 2004) specialized for cost-optimal reachability for theextended model of so-called priced timed automata.<br/
EXPERTISE & THE EURO
No full textThis project is about the experts role in the debate of the EMU referendum in 2000 in Denmark. This project use Faoucauldian theory as presented by Foucault, Rose & Miller and the concept of Epistemic Communities of Haas to analyse how three cases influenced the debate. The three cases chosen are: Danish Industry, Nationernes Europa and the Economic Counsel. This project have a post- structuralist epistemology and a constructionist ontology because of the chosen theory. After an analysis combining the theory with the empirical data about the cases the project concludes that the specific case of Nationernes Europa is an example of experts being able to influence subjects indirectly.This project is about the experts role in the debate of the EMU referendum in 2000 in Denmark. This project use Faoucauldian theory as presented by Foucault, Rose & Miller and the concept of Epistemic Communities of Haas to analyse how three cases influenced the debate. The three cases chosen are: Danish Industry, Nationernes Europa and the Economic Counsel. This project have a post- structuralist epistemology and a constructionist ontology because of the chosen theory. After an analysis combining the theory with the empirical data about the cases the project concludes that the specific case of Nationernes Europa is an example of experts being able to influence subjects indirectly
Almost Optimal Strategies in One Clock Priced Timed Automata
No full textInternational audienceWe consider timed games extended with cost information, and prove computability of the optimal cost and of -optimal memoryless strategies in timed games with one~clock. In~contrast, this problem has recently been proved undecidable for timed games with three clocks
A Formalization of Linkage Analysis
No full textIn this report a formalization of genetic linkage analysis is introduced. Linkage analysis is a computationally hard biomathematical method, which purpose is to locate genes on the human genome. It is rooted in the new area of bioinformatics and no formalization of the method has previously been established. Initially, the biological model is presented. On the basis of this biological model we establish a formalization that enables reasoning about algorithms used in linkage analysis. The formalization applies both for single and multi point linkage analysis. We illustrate the usage of the formalization in correctness proofs of central algorithms and optimisations for linkage analysis. A further use of the formalization is to reason about alternative methods for linkage analysis. We discuss the use of MTBDDs and PDGs in linkage analysis, since they have proven efficient for other computationally hard problems involving large state spaces. We conclude that none of the techniques discussed are directly applicable to linkage analysis, however further research is needed in order to investigated whether a modified version of one or more of these are applicable
