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.
In this paper, we consider multi-dimensional maximal costbounded reachability probability over continuous-time Markov decision processes (CTMDPs). Our major contributions are as follows. Firstly, we derive an integral...
详细信息
ISBN:
(纸本)9783642548307;9783642548291
In this paper, we consider multi-dimensional maximal costbounded reachability probability over continuous-time Markov decision processes (CTMDPs). Our major contributions are as follows. Firstly, we derive an integral characterization which states that the maximal cost-bounded reachability probability function is the least fixed-point of a system of integral equations. Secondly, we prove that the maximal cost-bounded reachability probability can be attained by a measurable deterministic cost-positional scheduler. thirdly, we provide a numerical approximation algorithm for maximal cost-bounded reachability probability. We present these results under the setting of both early and late schedulers. Besides, we correct a fundamental proof error in the PhD thesis by Martin Neuhaufier on maximal time-bounded reachability probability by completely new proofs for the more general case of multi-dimensional maximal cost-bounded reachability probability.
We establish foundational results on the computational complexity of deciding entailment in Separation Logic with general inductive predicates whose underlying base language allows for pure formulas, pointers and exis...
详细信息
ISBN:
(纸本)9783642548307;9783642548291
We establish foundational results on the computational complexity of deciding entailment in Separation Logic with general inductive predicates whose underlying base language allows for pure formulas, pointers and existentially quantified variables. We show that entailment is in general undecidable, and ExPTIME-hard in a fragment recently shown to be decidable by Iosif et al. Moreover, entailment in the base language is Pi(P)(2)-complete, the upper bound even holds in the presence of list predicates. We additionally show that entailment in essentially any fragment of Separation Logic allowing for general inductive predicates is intractable even when strong syntactic restrictions are imposed.
We study the relationship between two abstraction approaches for pointer programs, Separation Logic and hyperedge replacement grammars. Both employ inductively defined predicates and replacement rules, respectively, f...
详细信息
ISBN:
(纸本)9783319091082;9783319091075
We study the relationship between two abstraction approaches for pointer programs, Separation Logic and hyperedge replacement grammars. Both employ inductively defined predicates and replacement rules, respectively, for representing (dynamic) data structures, involving abstraction and concretisation operations for symbolic execution. In the Separation Logic case, automatically generating a complete set of such operations requires certain properties of predicates, which are currently implicitly described and manually established. In contrast, the structural properties that guarantee correctness of grammar abstraction are decidable and automatable. Using a property-preserving translation we argue that it is exactly the logic counterparts of those properties that ensure the direct applicability of predicate definitions for symbolic execution.
We study models of software systems with variants that stem from a specific choice of configuration parameters with a direct impact on performance properties. Using UML activity diagrams with quantitative annotations,...
详细信息
ISBN:
(纸本)9783642548048;9783642548031
We study models of software systems with variants that stem from a specific choice of configuration parameters with a direct impact on performance properties. Using UML activity diagrams with quantitative annotations, we model such systems as a product line. the efficiency of a product-based evaluation is typically low because each product must be analyzed in isolation, making difficult the re-use of computations across variants. Here, we propose a family-based approach based on symbolic computation. A numerical assessment on large activity diagrams shows that this approach can be up to three orders of magnitude faster than product-based analysis in large models, thus enabling computationally efficient explorations of large parameter spaces.
We present Comparator, a tool that measures the compatibility between two behavioural interfaces. Comparator can be used as a stand-alone Web application, and is also integrated into a model-based adaptation toolbox.
ISBN:
(纸本)9783642548048;9783642548031
We present Comparator, a tool that measures the compatibility between two behavioural interfaces. Comparator can be used as a stand-alone Web application, and is also integrated into a model-based adaptation toolbox.
the paper extends single-pushout graph transformation by polymorphism, a key concept in object-oriented design. the notions sub-rule and remainder, well-known in single-pushout rewriting, are applied in order to model...
详细信息
ISBN:
(纸本)9783642548048;9783642548031
the paper extends single-pushout graph transformation by polymorphism, a key concept in object-oriented design. the notions sub-rule and remainder, well-known in single-pushout rewriting, are applied in order to model dynamic rule extension and type dependent rule application. this extension mechanism qualifies graph transformation as a modelling technique for extendable frameworks. therefore, it contributes to the applicability of graph transformation in software engineering.
the automated analysis and verification of pointer-manipulating programs operating on a heap is a challenging task. It requires abstraction techniques for dealing with complex program behaviour and unbounded state spa...
详细信息
ISBN:
(纸本)9783319091082;9783319091075
the automated analysis and verification of pointer-manipulating programs operating on a heap is a challenging task. It requires abstraction techniques for dealing with complex program behaviour and unbounded state spaces that arise from both dynamic data structures and recursive procedures. In previous work it was shown that hyperedge replacement grammars provide an intuitive and versatile concept for defining and implementing such abstractions. Here we extend this approach towards a modular way of reasoning about programs with (possibly recursive) procedures featuring local variables. We propose an interprocedural dataflow analysis to automatically derive procedure contracts, i.e., graph transformations that concisely capture the overall effect of a procedure. Besides its modularity, another advantage of this analysis is that it relieves us from explicitly modelling the call stack on the heap, i.e., heap and control abstraction are clearly separated. the former can now be specified by simple and intuitive hyperedge replacement grammars describing the data structures only, while the latter is realised by automatically generated procedure contracts.
Stochastic rule-based models of networks and biological systems are hard to construct and analyse. Refinements help to produce systems at the right level of abstraction, enable analysis techniques and mappings to othe...
详细信息
ISBN:
(纸本)9783319091082;9783319091075
Stochastic rule-based models of networks and biological systems are hard to construct and analyse. Refinements help to produce systems at the right level of abstraction, enable analysis techniques and mappings to other formalisms. Rigidity is a property of graphs introduced in Kappa to support stochastic refinement, allowing to preserve the number of matches for rules in the refined system. In this paper: 1) we propose a notion of rigidity in an axiomatic setting based on adhesive categories;2) we show how the rewriting of rigid structures can be defined systematically by requiring matches to be open maps reflecting structural features which ensure that rigidity is preserved;and 3) we obtain in our setting a notion of refinement which generalises that in Kappa, and allows a rule to be partitioned into a set of rules which are collectively equivalent to the original. We illustrate our approach with an example of a social network with dynamic topology.
Reversible computation has attracted increasing interest in recent years, with applications in hardware, software and biochemistry. In this paper we show how to model reversibility in concurrent computation as realise...
详细信息
ISBN:
(纸本)9783319084947;9783319084930
Reversible computation has attracted increasing interest in recent years, with applications in hardware, software and biochemistry. In this paper we show how to model reversibility in concurrent computation as realised abstractly in terms of event structures. Two different forms of event structures are presented and it is shown how to extend them with reversibility.
暂无评论