the proceedings contain 32 papers from the foundations of softwarescience and computational structures, - 8thinternationalconference, FOSSACS 2005, held as part of the Joint European conferences on theory and Pract...
详细信息
the proceedings contain 32 papers from the foundations of softwarescience and computational structures, - 8thinternationalconference, FOSSACS 2005, held as part of the Joint European conferences on theory and Practices of software, ETAPS 2005, Proceedings. the topics discussed include: mathematical models of computational and combinatorial structures;probabilistic congruence for semistochastic generative processes;stochastic transition systems for continuous state spaces and non-determination;optimal conditional reachability fo multi-priced timed automata;and component refinement and CSC solving for STG decomposition.
We consider two-player reachability games with additional resource counters on arenas that are induced by the configuration graphs of pushdown systems. For a play, we define the resource cost to be the highest occurri...
详细信息
ISBN:
(纸本)9783642548307;9783642548291
We consider two-player reachability games with additional resource counters on arenas that are induced by the configuration graphs of pushdown systems. For a play, we define the resource cost to be the highest occurring counter value. In this way, we quantify resources and memory that player 0 needs to win. We introduce the bounded winning problem: Is there a uniform bound k such that player 0 can win the game from a set of initial configurations withthis bound k? We provide an effective, saturation-based method to solve this problem for regular sets of initial and goal configurations.
We consider infinite graphs that are generated by ground tree (or term) rewriting systems. the vertices of these graphs are trees. thus, with a finite tree automaton one can represent a regular set of vertices. It is ...
详细信息
ISBN:
(纸本)354043366X
We consider infinite graphs that are generated by ground tree (or term) rewriting systems. the vertices of these graphs are trees. thus, with a finite tree automaton one can represent a regular set of vertices. It is shown that for a regular set T of vertices the set of vertices from where one can reach (respectively, infinitely often reach) the set T is again regular. Furthermore it is shown that the problems, given a tree t and a regular set T, whether all paths starting in t eventually (respectively, infinitely often) reach T, are undecidable. We then define a logic which is in some sense a maximal fragment of temporal logic with a decidable model-checking problem for the class of ground tree rewriting graphs.
It is well-known that constructing models of higher-order probabilistic programming languages is challenging. We show how to construct step-indexed logical relations for a probabilistic extension of a higher-order pro...
详细信息
ISBN:
(纸本)9783662466780;9783662466773
It is well-known that constructing models of higher-order probabilistic programming languages is challenging. We show how to construct step-indexed logical relations for a probabilistic extension of a higher-order programming language with impredicative polymorphism and recursive types. We show that the resulting logical relation is sound and complete with respect to the contextual preorder and, moreover, that it is convenient for reasoning about concrete program equivalences. Finally, we extend the language with dynamically allocated first-order references and show how to extend the logical relation to this language. We show that the resulting relation remains useful for reasoning about examples involving both state and probabilistic choice.
Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifti...
详细信息
the traditional theory of "part of" relations (i.e. mereology) is enriched by adding the formal concept of equivalent and exchangeable parts. Various possible axioms and their roles are discussed. An approac...
详细信息
ISBN:
(纸本)3540287027
the traditional theory of "part of" relations (i.e. mereology) is enriched by adding the formal concept of equivalent and exchangeable parts. Various possible axioms and their roles are discussed. An approach is focused on application to model softwarestructures.
there are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full...
详细信息
ISBN:
(纸本)9783031572302;9783031572319
there are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full termination. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination (AST) w.r.t. innermost rewriting to prove full AST of probabilistic term rewrite systems. these criteria also apply to other notions of termination like positive AST. We implemented and evaluated our new contributions in the tool AProVE.
We present a theory for slicing probabilistic imperative programs-containing random assignment and "observe" statements-represented as control flow graphs whose nodes transform probability distributions. We ...
详细信息
ISBN:
(纸本)9783662496305;9783662496299
We present a theory for slicing probabilistic imperative programs-containing random assignment and "observe" statements-represented as control flow graphs whose nodes transform probability distributions. We show that such a representation allows direct adaptation of standard machinery such as data and control dependence, postdominators, relevant variables, etc. to the probabilistic setting. We separate the specification of slicing from its implementation: first we develop syntactic conditions that a slice must satisfy;next we prove that any such slice is semantically correct;finally we give an algorithm to compute the least slice. A key feature of our syntactic conditions is that they involve two disjoint slices such that the variables of one slice are probabilistically independent of the variables of the other. this leads directly to a proof of correctness of probabilistic slicing.
Graph Transformations provide a uniform and precise frame- work for the specification of access control policies allowing the detailed comparison of different policy models and the precise description of the evolution...
详细信息
We show that any one-counter automaton with n states, if its language is non-empty, accepts some word of length at most O(n(2)). this closes the gap between the previously known upper bound of O(n(3)) and lower bound ...
详细信息
ISBN:
(纸本)9783662496305;9783662496299
We show that any one-counter automaton with n states, if its language is non-empty, accepts some word of length at most O(n(2)). this closes the gap between the previously known upper bound of O(n(3)) and lower bound of Omega(n(2)). More generally, we prove a tight upper bound on the length of shortest paths between arbitrary configurations in one-counter transition systems (weaker bounds have previously appeared in the literature).
暂无评论