the proceedings contain 57 papers. the topics discussed include: a new analysis of expected revenue: combinatorial and simultaneous auctions;can component/service-based systems be proved correct?;probabilitic acceptor...
ISBN:
(纸本)3540958908
the proceedings contain 57 papers. the topics discussed include: a new analysis of expected revenue: combinatorial and simultaneous auctions;can component/service-based systems be proved correct?;probabilitic acceptors for languages over infinite words;automatic verification of heap manipulation using separation logic;randomness and determination, from physics and computing toward biology;when analysis fails: heuristic mechanism design via self-correcting procedures;on compositionality, efficiency, and applicability of abstraction in probabilistic systems;framed versus unframed two-dimensional languages;approximating tree edit distance through string edit distance for binary tree codes;the shortcut problem - complexity and approximation;green computing: energy consumption optimized service hosting;natural specifications yield decidability for distributed synthesis of asynchronous systems;and epistemic strategies and games on concurrent processes.
Probabilistic omega-automata are variants of nondeterministic automata for infinite words where all choices are resolved by probabilistic distributions. Acceptance of an infinite input word requires that the probabili...
详细信息
ISBN:
(纸本)9783540958901
Probabilistic omega-automata are variants of nondeterministic automata for infinite words where all choices are resolved by probabilistic distributions. Acceptance of an infinite input word requires that the probability for the accepting runs is positive. In this paper, we provide a summary of the fundamental properties of probabilistic omega-automata concerning expressiveness, efficiency, compositionality and decision problems.
the transitions of a stateless automaton do not depend on internal states but. solely on the symbols currently scanned by its heads accessing the input. or memory. We investigate stateless deterministic restarting aut...
详细信息
ISBN:
(纸本)9783540958901
the transitions of a stateless automaton do not depend on internal states but. solely on the symbols currently scanned by its heads accessing the input. or memory. We investigate stateless deterministic restarting automata that, after executing a rewrite step, Continue to read their tape before. performing a restart. Even the weakest class thus obtained contains the regular languages properly. the relations between different classes of stateless automata as well as between stateless automata and the corresponding types of automata with states are investigated, and it is shown that the language classes defined by the various types of deterministic stateless restarting automata without Auxiliary symbols are anti-AFLs that are not even closed under reversal.
this book constitutes the refereed proceedings of the 35th conference on current trends in theory and practice of computer science, sofsem 2009, held in pindleruv Mln, Czech Republic, in January 2009. the 49 revised f...
ISBN:
(数字)9783540958918
ISBN:
(纸本)9783540958901
this book constitutes the refereed proceedings of the 35th conference on current trends in theory and practice of computer science, sofsem 2009, held in pindleruv Mln, Czech Republic, in January 2009. the 49 revised full papers, presented together with 9 invited contributions, were carefully reviewed and selected from 132 submissions. sofsem 2009 was organized around the following four tracks: Foundations of computerscience; theory and practice of Software Services; Game theoretic Aspects of E-commerce; and Techniques and Tools for Formal Verification.
During the last years, speed-up techniques for DIJKSTRA's algorithm have been developed that make the computation of shortest paths a matter of microseconds even oil huge road networks. the most sophisticated meth...
详细信息
ISBN:
(纸本)9783540958901
During the last years, speed-up techniques for DIJKSTRA's algorithm have been developed that make the computation of shortest paths a matter of microseconds even oil huge road networks. the most sophisticated methods enhance the graph by inserting shortcuts, i.e. additional edges, that represent shortest paths in the graph. Until now, all existing shortcut-insertion strategies are heuristics and no theoretical results on the topic are known. In this work, we formalize the problem of adding shortcuts as a graph augmentation problem, study the algorithmic complexity of the problem, give approximation algorithms and show how to stochastically evaluate a given shortcut assignment on graphs that are too big to evaluate it exactly.
Microcontroller software typically consists of a few hundred lines of code only, but, it is rather different from standard application code.. the software is highly hardware and platform specific, and bugs are often a...
详细信息
ISBN:
(纸本)9783540958901
Microcontroller software typically consists of a few hundred lines of code only, but, it is rather different from standard application code.. the software is highly hardware and platform specific, and bugs are often a consequence of neglecting subtle specifications of the microcontroller architecture. currently, there are hardly any tools for analyzing such software automatically. Tu this paper, we outline Specifies of microcontroller software that explain why those programs are different to standard C/C++ code. We develop a static program analysis for a specific microcontroller, in our case the ATmega16, to spot code deficiencies, and integrate it into our generic static analyzer Comma. Finally, we illustrate the results by a case study of an automotive application. the case study highlights that even without formal proof the proposed static techniques can be valuable in pinpointing software bugs that are otherwise hard to find.
We study the rendezvous problem in the asynchronous setting in the graph of infinite line following the model introduced in [13]. We formulate general lemmas about deterministic rendezvous algorithms in this setting w...
详细信息
ISBN:
(纸本)9783540958901
We study the rendezvous problem in the asynchronous setting in the graph of infinite line following the model introduced in [13]. We formulate general lemmas about deterministic rendezvous algorithms in this setting which characterize the algorithms in which the agents have the shortest routes. We also improve rendezvous algorithms in the infinite line which formulated in [13]. Two agents have distinct labels L-min, L-max and vertical bar L-min vertical bar <= vertical bar L-max vertical bar. When the initial distance D between the agents is known, our algorithm has cost D vertical bar L-min vertical bar(2) which is ail improvement in the constant. If the initial distance is unknown we give an algorithm of cost O(D log(2) D + D log D vertical bar L-max vertical bar + D vertical bar L-min vertical bar(2) + vertical bar L-max vertical bar vertical bar L-min vertical bar log vertical bar L-min vertical bar) which is an asymptotic improvement.
the problem of finding k minimum energy, edge-disjoint paths in wireless networks (MEEP) arises in the context of routing and belongs to the class of range assignment problems. A polynomial algorithm which guarantees ...
详细信息
ISBN:
(纸本)9783540695066
the problem of finding k minimum energy, edge-disjoint paths in wireless networks (MEEP) arises in the context of routing and belongs to the class of range assignment problems. A polynomial algorithm which guarantees a factor-k-approximation for this problem has been presented before, but its complexity status was open. In this paper we prove that MEEP is NP-hard and give new lower and upper bounds on the approximation factor of the k-approximation algorithm. For MEEP on acyclic graphs we introduce an exact, polynomial algorithm which is then extended to a heuristic for arbitrary graphs.
Sufficient conditions for the existence and uniqueness of smooth optimal decision strategies for static team optimization problems with statistical information structure are derived. Approximation methods and algorith...
详细信息
ISBN:
(纸本)9783642112652
Sufficient conditions for the existence and uniqueness of smooth optimal decision strategies for static team optimization problems with statistical information structure are derived. Approximation methods and algorithms to derive suboptimal solutions based on the obtained results are investigated. the application to network team optimization problems is discussed.
this paper presents a complete account of positive and negative results on the finite axiomatizability of weak complete simulation semantics over the language BCCSP. We offer finite (un)conditional ground-complete axi...
详细信息
ISBN:
(纸本)9783642276590;9783642276606
this paper presents a complete account of positive and negative results on the finite axiomatizability of weak complete simulation semantics over the language BCCSP. We offer finite (un)conditional ground-complete axiomatizations for the weak complete simulation pre-congruence. In sharp contrast to this positive result, we prove that, in the presence of at least one observable action, the (in)equational theory of the weak complete simulation precongruence over BCCSP does not have a finite (in)equational basis. In fact, the set of (in)equations in at most one variable that hold in weak complete simulation semantics over BCCSP does not have an (in)equational basis of 'bounded depth', let alone a finite one.
暂无评论