the implementation of Building Information modelling (BIM) methodology in the construction industry has been covering a wide applicability with recognized benefits in designing, constructing and operating buildings. A...
详细信息
Data fusion and integration is an important subject for coal enterprises to develop and utilize coalbed gas. In the current situation of the shortage of coalbed gas database resources and analysistools in China’s co...
详细信息
Rapid and reliable diagnosis of cerebral stroke is a vital necessity, and among them, ischemic stroke is the most difficult to recognize on MRI images. Increasing the efficiency of stroke diagnosis is associated with ...
详细信息
Withthe gradual development of new distribution system, the standard of traditional distribution system has appeared lag, so people need to explore the standard demand of new distribution system. this paper mainly di...
详细信息
We consider the problem: is the optimal expected total re- ward to reach a goal state in a partially observable Markov decision process (POMDP) below a given threshold? We tackle this-generally undecidable-problem by ...
详细信息
ISBN:
(纸本)9783030995270;9783030995263
We consider the problem: is the optimal expected total re- ward to reach a goal state in a partially observable Markov decision process (POMDP) below a given threshold? We tackle this-generally undecidable-problem by computing under-approximations on these total expected rewards. this is done by abstracting finite unfoldings of the infinite belief MDP of the POMDP. the key issue is to find a suitable under-approximation of the value function. We provide two techniques: a simple (cut-off) technique that uses a good policy on the POMDP, and a more advanced technique (belief clipping) that uses minimal shifts of probabilities between beliefs. We use mixed-integer linear programming (MILP) to find such minimal probability shifts and experimentally show that our techniques scale quite well while providing tight lower bounds on the expected total reward.
While model checking safety of infinite-state systems by inferring state invariants has steadily improved recently, most verification tools still rely on a technique based on bounded model checking to detect safety vi...
详细信息
ISBN:
(纸本)9783030995249;9783030995232
While model checking safety of infinite-state systems by inferring state invariants has steadily improved recently, most verification tools still rely on a technique based on bounded model checking to detect safety violations. In particular, the current techniques typically analyze executions by unfolding transitions one step at a time, and the slow growth of execution length prevents detection of deep counterexamples before the tool reaches its limits on computations. We propose a novel model-checking algorithm that is capable of both proving unbounded safety and finding long counterexamples. the idea is to use Craig interpolation to guide the creation of symbolic abstractions of exponentially longer sequences of transitions. Our experimental analysis shows that on unsafe benchmarks with deep counterexamples our implementation can detect faulty executions that are at least an order of magnitude longer than those detectable by the state-of-the-art tools.
FRAMA-C is a well-known platform for source-code analysis of programs written in C. It can be extended via its plug-in architecture by various analysis backends and features an extensive annotation language called ACS...
详细信息
ISBN:
(纸本)9783030995270;9783030995263
FRAMA-C is a well-known platform for source-code analysis of programs written in C. It can be extended via its plug-in architecture by various analysis backends and features an extensive annotation language called ACSL. So far it was hard to compare FRAMA-C to other software verifiers. Our competition participation contributes an adapter named FRAmA-c-sv, which makes it possible to evaluate FRAMA-C against other software verifiers. the adapter transforms standard verification tasks (from the well-known SV-Benchmarks collection) in a way that can be understood by FRAMA-C and produces a verification witness as output. While FRAMA-C provides many different analyses, we focus on the Evolved Value analysis (EVA), which uses a combination of different domains to over-approximate the behavior of the analyzed program.
Withthe rapid development of space technology, the demand for landing applications of space-based information in various fields is becoming stronger and stronger. the traditional processing strategy of transmitting s...
详细信息
Game-theoretic techniques and equilibria analysis facilitate the design and verification of competitive systems. While algorithmic complexity of equilibria computation has been extensively studied, practical implement...
详细信息
ISBN:
(纸本)9783030995270;9783030995263
Game-theoretic techniques and equilibria analysis facilitate the design and verification of competitive systems. While algorithmic complexity of equilibria computation has been extensively studied, practical implementation and application of game-theoretic methods is more recent. tools such as PRISM-games support automated verification and synthesis of zero-sum and (epsilon-optimal subgame-perfect) social welfare Nash equilibria properties for concurrent stochastic games. However, these methods become inefficient as the number of agents grows and may also generate equilibria that yield significant variations in the outcomes for individual agents. We extend the functionality of PRISM-games to support correlated equilibria, in which players can coordinate through public signals, and introduce a novel optimality criterion of social fairness, which can be applied to both Nash and correlated equilibria. We show that correlated equilibria are easier to compute, are more equitable, and can also improve joint outcomes. We implement algorithms for both normal form games and the more complex case of multi-player concurrent stochastic games with temporal logic specifications. On a range of case studies, we demonstrate the benefits of our methods.
Many safety critical systems guarantee fault-tolerance by using several redundant copies of their components. When designing such redundancy architectures, it is crucial to analyze their fault trees, which describe co...
详细信息
ISBN:
(纸本)9783030995270;9783030995263
Many safety critical systems guarantee fault-tolerance by using several redundant copies of their components. When designing such redundancy architectures, it is crucial to analyze their fault trees, which describe combinations of faults of individual components that may cause malfunction of the system. State-of-the-art techniques for fault tree computation use first-order formulas with uninterpreted functions to model the transformations of signals performed by the redundancy system and an AllSMT query for computation of the fault tree from this encoding. Scalability of the analysis can be further improved by techniques such as predicate abstraction, which reduces the problem to Boolean case. In this paper, we show that as far as fault trees of redundancy architectures are concerned, signal transformation can be equivalently viewed in a purely Boolean way as fault propagation. this alternative view has important practical consequences. First, it applies also to general redundancy architectures with cyclic dependencies among components, to which the current state-of-the-art methods based on AIISMT are not applicable, and which currently require expensive sequential reasoning. Second, it allows for a simpler encoding of the problem and usage of efficient algorithms for analysis of fault propagation, which can significantly improve the runtime of the analyses. A thorough experimental evaluation demonstrates the superiority of the proposed techniques.
暂无评论