# (参考訳) 確率的プログラムのための帰納的合成 [全文訳有]

Inductive Synthesis for Probabilistic Programs Reaches New Horizons ( http://arxiv.org/abs/2101.12683v1 )

ライセンス: CC BY 4.0
Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen(参考訳) 本稿では,確率的プログラムの自動合成手法を提案する。 開始点は、関連するが明確な位相を持つ有限状態マルコフ鎖の有限族を表すプログラムスケッチと、PCTL仕様である。 この方法は、プログラムに違反するための反例(CE)を熱心に生成し、それらを家族をプルーニングするために使用する新しい誘導性オラクルの上に構築される。 これらの CE は、MDP 抽象化を使用して導関数によって提供される最良および最悪の振る舞いの境界という形で、家族のセマンティクスを活用します。 さらに、合成性能を監視し、インダクティブ推論とインダクティブ推論を適応的に切り替える。 実験により,新しいCE構造はより高速で効率的なプルーニング戦略を提供し,幅広いベンチマーク上での合成プロセスの高速化につながることが示された。 分散化された部分観測可能なコントローラの合成など,困難な問題に対して,実行時間を1日から数分に短縮する。

This paper presents a novel method for the automated synthesis of probabilistic programs. The starting point is a program sketch representing a finite family of finite-state Markov chains with related but distinct topologies, and a PCTL specification. The method builds on a novel inductive oracle that greedily generates counter-examples (CEs) for violating programs and uses them to prune the family. These CEs leverage the semantics of the family in the form of bounds on its best- and worst-case behaviour provided by a deductive oracle using an MDP abstraction. The method further monitors the performance of the synthesis and adaptively switches between the inductive and deductive reasoning. Our experiments demonstrate that the novel CE construction provides a significantly faster and more effective pruning strategy leading to acceleration of the synthesis process on a wide range of benchmarks. For challenging problems, such as the synthesis of decentralized partially-observable controllers, we reduce the run-time from a day to minutes.
公開日: Fri, 29 Jan 2021 16:59:00 GMT

※ 翻訳結果を表に示しています。PDFがオリジナルの論文です。翻訳結果のライセンスはCC BY-SA 4.0です。詳細はトップページをご参照ください。


    Page: /      
1 2 0 2 n a J 1 2 0 2 n a J 0.85
9 2 ] O L . 9 2 ] O L。 0.81
s c [ 1 v 3 8 6 2 1 sc [ 1 v 3 8 6 2 1 0.68
. 1 0 1 2 : v i X r a . 1 0 1 2 : v i X r a 0.85
Inductive Synthesis for Probabilistic Programs 確率的プログラムの帰納的合成 0.72
Reaches New Horizons(cid:63) Reaches New Horizons (cid:63) 0.91
Roman Andriushchenko1 Sebastian Junges2 Roman Andriushchenko1 Sebastian Junges2 0.84
, Milan ˇCeˇska ((cid:66))1 , and Joost-Pieter Katoen3 ミラノ・シケシュカ(cid:66)1,joost-piet er katoen3 0.61
, 1 Brno University of Technology, Brno, Czech Republic , 1 Brno University of Technology, Brno, チェコ共和国。 0.89
ceskam@fit.vutbr.cz ceskam@fit.vutbr.cz 0.59
2 University of California, Berkeley, USA カリフォルニア大学バークレー校2年生。 0.61
3 RWTH Aachen University, Aachen, Germany 3 RWTH アーヘン大学、アーヘン、ドイツ。 0.71
Abstract. This paper presents a novel method for the automated synthesis of probabilistic programs. 抽象。 本稿では,確率的プログラムの自動合成手法を提案する。 0.72
The starting point is a program sketch representing a finite family of finite-state Markov chains with related but distinct topologies, and a reachability specification. 出発点は、関連するが異なる位相を持つ有限状態マルコフ連鎖の有限族と到達可能性仕様を表すプログラムスケッチである。 0.72
The method builds on a novel inductive oracle that greedily generates counter-examples (CEs) for violating programs and uses them to prune the family. この方法は、プログラムに違反するための反例(CE)を熱心に生成し、それらを家族をプルーニングするために使用する新しい誘導性オラクルの上に構築される。 0.50
These CEs leverage the semantics of the family in the form of bounds on its bestand worst-case behaviour provided by a deductive oracle using an MDP abstraction. これらの CE は、MDP 抽象化を使用して導関数によって提供される最悪の振る舞いに対して、ファミリーの意味論を境界の形で活用します。 0.56
The method further monitors the performance of the synthesis and adaptively switches between inductive and deductive reasoning. さらに、合成性能を監視し、インダクティブ推論とインダクティブ推論を適応的に切り替える。 0.56
Our experiments demonstrate that the novel CE construction provides a significantly faster and more effective pruning strategy leading to an accelerated synthesis process on a wide range of benchmarks. 実験により,新しいCE構造により,より高速で効率的なプルーニング戦略が実現され,幅広いベンチマーク上での高速な合成プロセスが実現された。 0.74
For challenging problems, such as the synthesis of decentralized partially-observable controllers, we reduce the run-time from a day to minutes. 分散化された部分観測可能なコントローラの合成など,困難な問題に対して,実行時間を1日から数分に短縮する。 0.62
1 Introduction Background and motivation. 1 はじめに 背景とモチベーション。 0.67
Controller synthesis for Markov decision processes (MDPs [35]) and temporal logic constraints is a well-understood and tractable problem, with a plethora of mature tools providing efficient solving capabilities. マルコフ決定プロセス(MDP [35])と時間論理制約のためのコントローラ合成は、効率的な解決機能を提供する多数の成熟したツールで、よく理解され、牽引可能な問題です。 0.67
However, the applicability of these controllers to a variety of systems is limited: Systems may be decentralized, controllers may not be able to observe the complete system state, cost constraints may apply, and so forth. しかし、これらのコントローラのさまざまなシステムへの適用可能性は限られている:システムは分散化され、コントローラは完全なシステム状態を観察できない、コスト制約が適用される、など。 0.79
Adequate operational models for these systems exist in the form of decentralized partially-observable MDPs (DEC-POMDPs [33]). これらのシステムの適切な運用モデルは、分散部分可観測 MDP (DEC-POMDPs [33]) の形で存在する。 0.73
The controller synthesis problem for these models is undecidable [30], and tool support (for verification tasks) is scarce. これらのモデルのコントローラ合成問題は[30]決定不能であり、ツールサポート(検証タスク)は不十分である。 0.77
This paper takes a different approach: the controller together with the environment can be modelled as probabilistic program sketches where “holes” in the probabilistic program model choices that the controller may make. この論文では、コントローラと環境は、コントローラが行う可能性のある確率的プログラムモデル選択の「穴」を確率的プログラムスケッチとしてモデル化することができる。 0.77
Conceptually, the controllers of the DEC-POMDP are described by a user-defined finite 概念上、DEC-POMDPのコントローラはユーザ定義有限で記述される。 0.75
(cid:63) This work has been partially supported by the Czech Science Foundation grant GJ20-02328Y and the ERC AdG Grant 787914 FRAPPANT, the NSF grants 1545126 (VeHICaL) and 1646208, by the DARPA Assured Autonomy program, by Berkeley Deep Drive, and by Toyota under the iCyPhy center. (cid:63) この研究は、チェコ科学財団の助成金GJ20-02328YとERC AdG Grant 787914 FRAPPANT、NSFの助成金1545126(VeHICaL)と1646208、DARPA Asured Autonomyプログラム、バークレーディープドライブ、およびトヨタのiCyPhyセンターによって部分的に支持されています。 0.78
Consistent * Complete * Well Documented * Easy to Reuse * * Evaluated * TACAS * Artifact * AEC Consistent * Complete * Well Documented * Easy to Reuse * * Evaluated * TACAS * Artifact * AEC 0.85
2 R. Andriushchenko et al. 2 r. andriushchenkoら。 0.77
family M of Markov chains. マルコフチェーンのファミリーM。 0.59
The synthesis problem that we consider is to find a Markov chain M (i.e., a probabilistic program) in the family M, such that M |= ϕ, where ϕ is the specification. 我々が考慮する合成問題は、M |= φ が仕様であるような、ファミリー M にマルコフ鎖 M (すなわち確率的プログラム) を見つけることである。
訳抜け防止モード: 私たちが考える合成問題はマルコフ連鎖 M(すなわち、マルコフ連鎖)を見つけることである。 ファミリーMにおける確率的プログラム) M |= φ, ここで φ は仕様である。
To allow efficient algorithms, the family must have some structure. 効率的なアルゴリズムを可能にするために、家族は何らかの構造を持つ必要がある。 0.54
In particular, in our setting, the family is parameterized by a set of discrete parameters K; an assignment K → V of these parameters with concrete values V from its associated domain yields a family member, i.e., a Markov chain (MC). 特に、我々の設定では、族は離散パラメータ K の集合でパラメータ化される:これらのパラメータの割り当て K → V とその関連する領域からの具体的な値 V は、家族、すなわちマルコフ連鎖(MC)を生成する。 0.85
Such a parameterization is naturally obtained from the probabilistic program sketch, where some constants (or program parts) can be left open. このようなパラメータ化は確率的プログラムスケッチから自然に得られ、ある定数(またはプログラム部分)は開かないようにすることができる。 0.72
The search for a family member can thus be considered as the search for a hole-assignment. したがって、家族のメンバーの検索は、ホール割り当ての検索と見なすことができます。 0.76
This approach fits within the realm of syntax-guided synthesis [2]. このアプローチは構文誘導合成 [2] の領域に適合する。 0.82
Motivating example. モチベーションの例。 0.58
Herman’s protocol [24] is a well-studied randomized distributed algorithm aimed to obtain fast stabilization on average. Hermanのプロトコル[24]は、平均的に速い安定化を得ることを目的としたよく研究されたランダム化分散アルゴリズムです。 0.68
In [26], a family M of MCs is used to model different protocol instances. 26]では、MCのファミリーMを使用して異なるプロトコルインスタンスをモデル化する。 0.75
They considered each instance separately, and found which of the controllers for Herman’s protocol performs best. 彼らは各インスタンスを別々に考慮し、hermanのプロトコルのどのコントローラがベストかを突き止めた。 0.71
Let us consider the protocol in a bit more detail: It considers self-stabilization of a unidirectional ring of network stations where all stations have to behave similarly—an anonymous network. プロトコルをもう少し詳しく考えてみましょう – すべてのステーションが同じように振る舞わなければならない一方向のネットワークステーションのリング — の自己安定化を考えるのです。 0.69
Each station stores a single bit, and can read the internal bit of one (say left) neighbour. 各駅は1ビットを格納し、1つの(例えば左)隣人の内部のビットを読むことができる。 0.77
To achieve stabilization, a station for which the two legible bits coincide updates its own bit based on the outcome of a coin flip. 安定化を実現するために、2つのレジブルビットが一致するステーションは、コインフリップの結果に基づいて自ビットを更新する。 0.73
The challenge is to select a controller that flips this coin with an optimal bias, i.e., minimizing the expected time until stabilization. 問題は、このコインを最適バイアスで反転させるコントローラ、すなわち安定化までの期待時間を最小化することである。 0.74
In a setting where the probabilities range over 0.1, 0.2, . 確率が0.1以上、0.2以上である場合。 0.58
. . , 0.9, this results in analyzing nine different MCs. . . 0.9では9つの異なるMCを解析できる。 0.81
Does the expected time until stabilization reduce if the controllers are additionally allowed to have a single bit of memory? コントローラに1ビットのメモリが加わった場合、安定化までの期待時間が短縮されますか? 0.79
In every step, there are 9·9 combinations for selecting the coin flip and for each memory cell and coin flip outcome, the memory can now be updated, yielding 2·2·2 possibilities. 各ステップにおいて、コインフリップを選択する9·9の組み合わせがあり、各メモリセルとコインフリップの結果に対して、メモリを更新でき、2·2·2の可能性が得られる。 0.66
This one-bit extension thus results in a family of 648 models. この1ビット拡張により、648のモデル群が得られる。 0.72
If, in addition, one allows stations to make decisions depending on the token-bits, both the coin flips and the memory updates are multiplied by a factor 4, yielding 10, 368 models. さらに、トークンビットに応じてステーションが決定できるようにすると、コインフリップとメモリ更新の両方がファクタ4に乗じられ、10,368モデルが生成される。 0.59
Eventually, analyzing all individual MCs is infeasible. 最終的に、個々のmcsを分析することは不可能である。 0.45
Oracle-guided synthesis. oracle による合成。 0.62
To tackle the synthesis problem, we introduce an oracleguided inductive synthesis approach [25,39]. 合成問題に取り組むために, oracleguided inductive synthesis approach [25,39] を導入する。 0.90
A learner selects a family member and passes it to the oracle. 学習者は家族を選択し、それをオラクルに渡します。 0.73
The oracle answers whether the family member satisfies ϕ, and crucially, gives additional information in case this is not the case. オラクルは、家族がφを満たすかどうかを答え、決定的に、そうでない場合は追加情報を与える。 0.69
Inspired by [9], if the family member violates the specification ϕ, our oracle returns a set K(cid:48) of parameters such that all family members obtained by changing only the values assigned to K(cid:48) violate ϕ. 9]にインスパイアされた私たちのオラクルは、家族メンバーが仕様 φ に反した場合、K(cid:48) に割り当てられた値だけを変更して得られるすべての家族メンバーが φ に反するようなパラメータの集合 K(cid:48) を返す。 0.74
We argue that such an oracle must (1) induce little overhead in providing K(cid:48), (2) be aware of the existence of parameters in the family, and (3) have (resemblance of) awareness about the semantics of the parameters and their values. このようなオラクルは,(1)K(cid:48)の提供においてほとんどオーバーヘッドを生じさせないこと,(2)家族内のパラメータの存在を意識すること,(3)パラメータのセマンティクスとそれらの値について(再)意識を持つこと,などを議論する。 0.78
Oracles. With these requirements in mind, we construct a counterexample (CE)based oracle from scratch. Oracle。 これらの要件を念頭に置いて,ceベースのoracleをスクラッチから構築しています。 0.61
We do so by carefully exploiting existing methods. 私たちは既存の方法を慎重に活用する。 0.66
We construct critical subsystems as CEs [1]. CE [1] として重要なサブシステムを構築します。 0.59
Critical subsystems are parts of 重要なサブシステムは 0.64
Inductive Synthesis for Probabilistic Programs Reaches New Horizons 確率的プログラムのための帰納的合成 0.65
3 the MC that suffice to refute the specification. 3 MCは仕様に反論するのに十分です 0.79
If a hole is absent in a CE, its value is irrelevant. CEに穴がなければ、その値は無関係である。 0.74
To avoid the cost of finding optimal CEs—an NP-hard problem [19]—we consider greedy CEs that are similar to [9]. 最適CE(NPハード問題[19])を見つけるコストを回避するため、[9]に類似した欲求CEを検討する。 0.70
However, our greedy CEs are aware of the parameters, and try to limit the occurrence of parameters in the CE. しかし、我々のgreedy CEはパラメータを認識しており、CE内でのパラメータの発生を制限しようと試みています。 0.71
Finally, to provide awareness of the semantics of parameter values, we provide lower and upper bounds on all states: Their difference indicates how much varying the value at a hole may change the overall reachability probability. 最後に、パラメータ値のセマンティクスを認識させるために、私たちはすべての状態に対して下限と上限を提供します。それらの違いは、穴の値がどれだけ変化するかを示し、全体的な到達可能性の確率を変えます。
訳抜け防止モード: 最後に、パラメータ値の意味を意識する。 すべての州に下限と上限を与えます それらの差は、ホールにおける値の変動が全体の到達可能性の確率を変化させることを示している。
These bounds are efficiently computed by another oracle. これらの境界は別のオラクルによって効率的に計算される。 0.48
This oracle analyses a quotient MDP obtained by employing an abstraction method that is part of the abstraction-refinement loop in [10]. この oracle は [10] の抽象再定義ループの一部である抽象法を用いて得られる商 MDP を解析します。 0.78
A hybrid variant. The two oracles are significantly different. ハイブリッド型。 2つの神託は著しく異なる。 0.51
Abstraction refinement is deductive: it argues about single family members by considering (an aggregation of) all family members. 抽象化の洗練は誘惑的であり、家族全員を考慮(集約)することによって、単一家族について論じる。 0.63
The critical subsystem oracle is inductive: by examining a single family member, it infers statements about other family members. 重要なサブシステム oracle は帰納的であり、単一のファミリーメンバーを調べることで、他のファミリーメンバーに関するステートメントを推論する。
訳抜け防止モード: 臨界サブシステムオラクルは誘導的です : 一人の家族を調べることで、他の家族の発言を推測する。
This suggests a middle ground: a hybrid strategy monitors the performance of the two oracles during the synthesis and suggests their best usage. ハイブリッド戦略(hybrid strategy)は、合成中の2つのオラクルのパフォーマンスを監視し、最適な使用法を提案する。
訳抜け防止モード: これは中盤を示唆している。 The hybrid strategy monitors the performance of the two oracles during the synthesis and suggests their best use。
More precisely, the hybrid strategy integrates the counterexample-based oracle into the abstraction-refinement loop. より正確には、ハイブリッド戦略は、反例に基づくオラクルを抽象化・リファインメントループに統合する。 0.53
Major results. We present a novel and dedicated oracle deployed in an efficacious synthesis loop. 主な結果。 効率的な合成ループに展開された新規で専用のオラクルを紹介します。 0.60
We use model-checking results on an abstraction to tailor smaller CEs. 抽象化のモデルチェック結果を使用して、より小さなCEをカスタマイズします。 0.51
Our greedy and family-aware CE construction is substantially faster than the use of optimal CEs. 私たちの欲求と家族を意識したCEの構築は、最適なCEを使用するよりもはるかに高速です。
訳抜け防止モード: 我らの欲と家族-自覚 CEの構成は最適なCEを使用するよりもかなり高速である。
Together, these two improvements yield CEs that are on par with optimal CEs, but are found much faster. これら2つの改良は、最適なCEと同等のCEを生成するが、より高速に発見される。 0.69
The integration of multiple abstraction-refinement steps yields a superior performance:x We compare our performance with the abstraction-refinement loop from [10] using benchmarks from [10]. 複数の抽象化・定義ステップの統合は、優れたパフォーマンスをもたらします。x ベンチマークを使用して、[10]の抽象化・定義ループとパフォーマンスを比較します。 0.66
Benchmarks can be classified along two dimensions: (A) Benchmarks with a structure good for CE-generation. ベンチマークは2つの次元に沿って分類できる: (A) CE世代に適した構造を持つベンチマーク。 0.62
(B) Benchmarks with a structure good for abstraction-refinement. (B)抽象化・リファインメントに適した構造を持つベンチマーク。 0.65
A-benchmarks are a natural strength of our novel oracle. A-benchmarksは私達の小説のoracleの自然な強さです。 0.61
Our simple, efficient hybrid strategy significantly outperforms the state-ofthe-art on A-benchmarks, while it only yields limited overhead for B-benchmarks. 当社のシンプルで効率的なハイブリッド戦略は、A-benchmarksの最先端のパフォーマンスを大幅に上回り、B-benchmarksのオーバーヘッドは限られています。 0.60
Most importantly, the novel hybrid strategy can solve benchmarks that are out of reach for pure abstraction-refinement or pure CE-based reasoning. 最も重要なのは、新しいハイブリッド戦略は、純粋に抽象的なリファインメントや純粋なCEベースの推論に到達できないベンチマークを解決できることだ。 0.55
In particular, our hybrid method is able to synthesize the optimal Herman protocol with memory—the synthesis time on a design space with 3.1 millions of candidate programs reduces from a day to minutes. 特に、我々のハイブリッド手法は最適なHermanプロトコルをメモリで合成することができ、設計空間における310万の候補プログラムによる合成時間は1日から数分に短縮される。 0.76
Related work The synthesis problems for parametric probabilistic systems can be divided into the following two categories. 関連する仕事 パラメトリック確率系の合成問題は以下の2つのカテゴリに分けられる。 0.83
Topology synthesis, akin to the problem considered in this paper, assumes a finite set of parameters affecting the MC topology. トポロジー合成は,本論文で検討した問題と同様に,mcトポロジーに影響を与える有限なパラメータの集合を仮定する。 0.79
Finding an instantiation satisfying a reachability property is NP-complete in the number of parameters [12], and can naively be solved by analyzing all individual family members. 到達可能性特性を満たすインスタンス化を見つけることはパラメーター[12]の数でnp完全であり、すべての家族を解析することによって自然に解決できる。
訳抜け防止モード: 到達性特性を満たすインスタンス化の探索 is NP - complete in the number of parameters [ 12 ] 個々の家族を 分析して 鼻で解決できるんです。
An alternative is to model the MC family by an MDP and resort to standard MDP modelchecking algorithms. 代替案は、MCファミリをMDPでモデル化し、標準のMDPモデルチェックアルゴリズムに頼ることである。 0.73
Tools such as ProFeat [13] or QFLan [40] take this approach ProFeat [13] や QFLan [40] のようなツールがこのアプローチを取る 0.87
4 R. Andriushchenko et al. 4 r. andriushchenkoら。 0.77
to quantitatively analyze alternative designs of software product lines [21,28]. ソフトウェア製品ライン[21,28]の代替設計を定量的に解析する。 0.75
These methods are limited to small families. これらの方法は小家族に限られる。 0.73
This motivated (1) abstractionrefinement over the MDP representation [10], and (2) counterexample-guide d inductive synthesis (CEGIS) for MCs [9], mentioned earlier. この動機付けは(1) MDP表現上の抽象化定義 [10] と(2) MCに対する逆例誘導誘導合成 (CEGIS) [9] である。 0.79
The alternative problem of sketching for probabilistic programs that fit given data is studied, e.g., in [32,38]. 与えられたデータに適合する確率的プログラムのスケッチの代替問題は、例えば[32,38]で研究される。 0.80
Parameter synthesis considers models with uncertain parameters associated to transition probabilities, and analyses how the system behaviour depends on the parameter values. パラメータ合成は、遷移確率に関連する不確実なパラメータを持つモデルを検討し、システムの振る舞いがパラメータ値に依存するかを分析する。 0.73
The most promising techniques are based on parameter lifting that treats identical parameters in different transitions independently [8,36] and has been implemented in the state-of-the-art probabilistic model checkers Storm [18] and PRISM [27]. 最も有望な技術は、異なる遷移における同一パラメータを独立して扱うパラメータリフティング [8,36] に基づいており、最新の確率モデルチェッカーStorm [18] および PRISM [27] で実装されています。 0.76
An alternative approach based on building rational functions for the satisfaction probability has been proposed in [15] and further improved in [22,17,4]. 満足度確率に対する有理関数構築に基づく別のアプローチが[15]で提案され、[22,17,4]でさらに改善されている。 0.76
This approach has been also applied to different problems such as model repair [5,34,11]. このアプローチは、モデル修復[5,34,11]など、さまざまな問題にも適用されています。 0.60
Both synthesis problems can be also attacked by search-based techniques that do not ensure an exhaustive exploration of the parameter space. 両方の合成問題は、パラメータ空間の徹底的な探索を保証することができない検索ベースの技術によっても攻撃される。 0.67
These include evolutionary techniques [23,31] and genetic algorithms [20]. これには進化技術 [23,31] と遺伝的アルゴリズム [20] が含まれる。 0.73
Combinations with parameter synthesis have been used [7] to synthesize robust systems. パラメータ合成と組み合わせて、ロバストなシステムを合成した[7]。 0.70
2 Problem Statement We formalize the essential ingredients and the problem statement. 2 問題声明 我々は本質的な要素と問題ステートメントを定式化する。 0.67
See [3] for more material. 詳細は[3]を参照。 0.55
µ : S → [0, 1] s.t. μ : S → [0, 1] s.t。 0.94
(cid:80) Sets of Markov chains. (cid:80) マルコフチェーンのセット。 0.68
A (discrete) distribution over a finite set X is a function x µ(x) = 1. 有限集合 X 上の(離散)分布は、関数 x μ(x) = 1 である。 0.81
The set Distr(X) contains all distributions over X. セット Distr(X) は X 上のすべての分布を含む。 0.87
The support of µ ∈ Distr(X) is supp(µ) = {x ∈ X | µ(x) > 0}. μ ∈ Distr(X) の支持は supp(μ) = {x ∈ X | μ(x) > 0} である。 0.86
Definition 1 (MC). A Markov chain (MC) is a tuple D = (S, s0, P ), where S is a finite set of states, s0 ∈ S is an initial state, and P : S → Distr(S) is a transition probability function. 定義1(MC)。 マルコフ鎖(MC)はタプル D = (S, s0, P) であり、S は状態の有限集合であり、s0 ∈ S は初期状態であり、P : S → Distr(S) は遷移確率関数である。 0.75
We write P (s, t) to denote P (s)(t). P (s)(t) を表すために P (s, t) と書く。 0.74
The state s is absorbing if P (s, s) = 1. 状態 s は P (s, s) = 1 ならば吸収される。 0.86
Let K denote a finite set of discrete parameters with finite domain Vk. K を有限領域 Vk を持つ離散パラメータの有限集合とする。 0.73
For brevity, we often assume that all domains are the same, and omit the subscript k. A realization r maps parameters to values in their domain, i.e., r : K → V . 簡潔性については、すべての領域が同じであると仮定し、サブスクリプト k を省略する。 実化 r は、その領域の値、すなわち r : K → V にパラメータをマッピングする。
訳抜け防止モード: 簡潔性については、すべてのドメインが同じであると仮定することが多い。 A realization r はパラメータをそれらの領域の値にマッピングします。 すなわち、r : K → V である。
Let RD denote the set of all realizations of a set D of MCs. RD は、MC の集合 D のすべての実現の集合を表す。 0.70
A K-parameterized set of MCs D(K) contains the MCs Dr, for every r ∈ RD. MCs D(K) の K-パラメータ化集合は、すべての r ∈ RD に対して MCs Dr を含む。 0.79
In Sect. 3, we give an operational model for such sets. 宗派。 3、我々はそのようなセットの運用モデルを与える。 0.49
In particular, realizations will fix the targets of transitions. 特に、実現は遷移のターゲットを固定する。 0.55
In our experiments, we describe these sets using the PRISM modelling language where parameters are described by undefined integer values. 実験では,パラメータを未定義整数値で記述するprismモデリング言語を用いて,これらの集合を記述する。 0.75
Properties and specifications. For simplicity, we consider (unbounded) reachability properties1. 特性および指定。 単純化のために、(無制限の)到達性プロパティを考える。 0.60
For a set T ⊆ S of target states, let P[D, s |= ♦T ] denote 1 Our implementation also supports expected reachability rewards. 対象状態の集合 T × S に対して、P[D, s |= sT ] を 1 とすると、我々の実装は期待される到達性報酬もサポートする。 0.55
Inductive Synthesis for Probabilistic Programs Reaches New Horizons 確率的プログラムのための帰納的合成 0.65
5 the probability in MC D to eventually reach some state in T when starting in the state s ∈ S. A property ϕ ≡ P(cid:46)(cid:47)λ[♦T ] with λ ∈ [0, 1] and (cid:46)(cid:47)∈ {≤,≥} expresses that the probability to reach T does relate to λ according to (cid:46)(cid:47). 5 状態 s ∈ S で始まるとき、最終的に T のある状態に達する MC D の確率。 λ ∈ [0, 1] および (cid:46)(cid:47)∈ {≤, ) を持つ性質 φ (cid:46)(cid:47)λ[\T ] は、T に到達する確率が (cid:46)(cid:47) に従って λ と関連していることを示す。 0.86
If (cid:46)(cid:47) = ≤, then ϕ is a safety property; otherwise, it is a liveness property. cid:46)(cid:47) = ≤ であれば、φ は安全性質であり、そうでなければ生きた性質である。 0.75
Formally, state s in MC D satisfies ϕ if P[D, s |= ♦T ] ≥ λ. 形式的には、mc d の状態 s が φ を満たすのは p[d, s |= st ] ≥ λ である。 0.69
The MC D satisfies ϕ if the above holds for its initial state. MC D は、上記が初期状態を保持する場合 φ を満たす。 0.82
A specification is a set of properties Φ = {ϕi}i∈I , and D |= Φ if ∀i ∈ I : D |= ϕi. 明細書は性質の集合であり、 φi ∈ I : D | = φi であるとき、D | = φi である。 0.81
Problem statement. The key problem statement in this paper is feasibility: 問題声明。 本論文の問題点は, 実現可能性である。 0.61
Given a parameterized set of Markov chains D(K) over parameters K and a specification Φ, find a realization r : K → V such that Dr |= Φ. パラメータ K 上のマルコフ鎖 D(K) のパラメータ化集合と、仕様 A を与えられたとき、ドクター |= K → V が成立する r : K → V を見つける。 0.76
When D is clear from the context, we often write r |= Φ to denote Dr |= Φ. D が文脈から明確であるとき、しばしば r |= s と書き、Dr |= s を表す。 0.77
We additionally consider the optimizing variant of the synthesis problem. さらに,合成問題の最適化についても考察する。 0.74
The maximal synthesis problem asks: given a maximizing property ϕmax ≡ P(cid:46)(cid:47)λ[♦T ], identify r∗ ∈ arg maxr∈RD {P[Dr |= ♦T ] | Dr |= Φ} provided it exists. 最大合成問題は次のものを求める: 最大化性質 φmax × P(cid:46)(cid:47)λ[*T ] を与えられたとき、それが存在すれば r ∈ arg maxr∈RD {P[Dr |= st ] | Dr |= s} を同定する。 0.73
The minimal synthesis problem is defined analogously. 最小合成問題も同様に定義される。 0.77
As the state space S, the set K of parameters, and their domains are all finite, the above synthesis problems are decidable. 状態空間 s、パラメータの集合 k、およびそれらの領域がすべて有限であるので、上記の合成問題は決定可能である。 0.78
One possible solution, called the one-by-one approach [14], considers each realization r ∈ RD. 1対1のアプローチ[14]と呼ばれる1つの可能な解は、各実現 r ∈ RD を考える。 0.66
The state-space and parameter-space explosion renders this approach unusable for large problems, necessitating the usage of advanced techniques that exploit the family structure. 状態空間とパラメータ空間の爆発は、このアプローチを大きな問題に利用できないようにし、家族構造を利用する高度な技術を使う必要がある。 0.65
3 Counterexample-Guide d Inductive Synthesis 3 対例誘導誘導合成 0.73
In this section, we recap a baseline for a counterexample-guide d inductive synthesis (CEGIS) loop, as put forward in [9]. 本項では,[9]で述べるように, 反例誘導帰納的合成 (CEGIS) ループのベースラインを再構成する。 0.72
In particular, we first instantiate an oracle-guided synthesis method, discuss an operational model for families, giving structure to the parameterized set of Markov chains, and finally detail the usage of CEs to create an oracle. 特に、まず、オラクル誘導合成法をインスタンス化し、家族の操作モデルについて議論し、マルコフ連鎖のパラメータ化された集合の構造を与え、最後に、オラクルを作成するためのCEの使用について詳述する。 0.57
Consider Fig. 1. A learner takes a set R of realizations, and has to find a realization Dr satisfying the specification Φ. 図を考える。 1. 学習者は実化の集合 R を受け取り、仕様を満足する実化 Dr を見つける必要がある。 0.77
The learner maintains (a symbolic representation of) a set Q ⊆ R of realizations that need to be checked. 学習者は、(象徴的な表現の)チェックする必要がある実現のセットQ / Rを維持します。 0.67
It iteratively asks the oracle whether a particular r ∈ Q is a solution. 反復的に、特定の r ∈ Q が解であるかどうかをオラクルに尋ねる。 0.65
If it is a solution, the oracle reports success. ソリューションであれば、oracleは成功を報告します。 0.79
Otherwise, the oracle returns a set R(cid:48) containing r and potentially more realizations all violating Φ. さもなくば、オラクルは r を含む集合 R(cid:48) を返却し、より多く実現される可能性がある。 0.62
The learner then prunes R(cid:48) from Q. 学習者はその後、QからR(cid:48)をプルーンする。 0.57
In Section 4, we focus on creating an efficient oracle that computes a set R(cid:48) (with r ∈ R(cid:48)) of realizations that are all violating Φ. 第4節では、我々は(r ∈ R(cid:48) の集合 R(cid:48) を計算できる効率的なオーラクルの作成に焦点を当てている。 0.73
In Section 5, we provide a more advanced framework that extends this method. 第5節では、このメソッドを拡張するより高度なフレームワークを提供します。 0.69
The remainder of this section lays the groundwork for these sections. このセクションの残りは、これらのセクションの土台になっている。 0.63
r ∈ R(cid:48) ⊆ R, R(cid:48) all violate Φ r ∈ R(cid:48) > R, R(cid:48) は、すべて s に反する。 0.73
Fig. 1. Oracle-guided synthesis フィギュア。 1. オラクル誘導合成 0.67
Oracle r |= Φ Oracle r |= 。 0.86
D, Φ R Learner d, φ R 学習者 0.69
no r |= Φ r ∈ R なし r |= φ r ∈ R 0.80
6 R. Andriushchenko et al. 6 r. andriushchenkoら。 0.77
Families of Markov chains To avoid the need to iterate over all realizations, an efficient oracle exploits some structure of the family. マルコフ連鎖の家族 すべての実現を反復する必要性を避けるために、効率的なオラクルは家族の構造を悪用する。 0.67
In this paper, we focus on sets of Markov chains having different topologies. 本稿では,異なる位相を持つマルコフ鎖の集合に注目した。 0.64
We explain our concepts using the operational model of families given in [10]. 10]で与えられた家族の運用モデルを用いて概念を説明する。 0.79
Our implementation supports (more expressive) PRISM programs with undefined integer constants. 私たちの実装は、未定義の整数定数を持つ(より表現力のある)PRISMプログラムをサポートします。 0.49
Definition 2 (Family of MCs). 定義2(MCの家族)。 0.64
A family of MCs is a tuple D = (S, s0, K,B) with S and s0 as before, K is a finite set of parameters with domains Vk ⊆ S for each k ∈ K, and B : S → Distr(K) is a family of transition probability functions. MCs の族は、S と s0 を持つタプル D = (S, s0, K,B) であり、K は各 k ∈ K に対して領域 Vk, S を持つパラメータの有限集合であり、B : S → Distr(K) は遷移確率関数の族である。 0.79
Function B of a family D of MCs maps each state to a distribution over parameters K. In the context of the synthesis of probabilistic models, these parameters represent unknown options or features of a system under design. MCのファミリーDの関数Bは、各状態をパラメータK上の分布にマッピングする。確率モデルの合成の文脈では、これらのパラメータは設計中のシステムの未知の選択肢または特徴を表している。 0.81
Realizations are now defined as follows. 実現は次のように定義される。 0.61
Definition 3 (Realization). 定義3 (Realization)。 0.73
A realization of a family D = (S, s0, K,B) of MCs is a function r : K → S s.t. MCs の族 D = (S, s0, K,B) の実現は、函数 r : K → S s.t である。 0.82
r(k) ∈ Vk, for all k ∈ K. We say that realization r k∈K,r(k)=s(cid:48) B(s)(k) for any pair of states s, s(cid:48) ∈ S. The set of all realizations of D is denoted as RD. r(k) ∈ Vk はすべての k ∈ K に対して成立する r k∈K,r(k)=s(cid:48) B(s)(k) は任意の状態 s, s(cid:48) ∈ S に対して成立する。
訳抜け防止モード: r(k ) ∈ Vk, for all k ∈ K. 任意の状態 s,s(cid:48) に対して r k∈K, r(k)=s(cid:48 ) B(s)(k ) を実現すると言う。 ) ∈ S。 D のすべての実現の集合は RD として表される。
induces MC Dr = (S, s0,Br) iff Br(s, s(cid:48)) =(cid:80) The set RD =(cid:81) induces MC Dr = (S, s0,Br) iff Br(s, s(cid:48)) =(cid:80) 集合RD =(cid:81) 0.96
k∈K Vk of all possible realizations is exponential in |K|. すべての可能実現の k∈K Vk は |K| において指数的である。 0.55
Counterexample-guide d oracles We first consider the feasibility synthesis for a single-property specification and later, cf. Counterexample-guide d oracles まず、単一プロパティ仕様の実現可能性合成について検討し、その後、cf。 0.55
Remark 1, generalize this to multiple properties and to optimal synthesis. remark 1は、これを複数の特性と最適な合成に一般化する。 0.67
The notion of counterexamples is at the heart of the oracle from [9] and Sect. 反例の概念は[9]および宗派からのオラクルの中心にあります。 0.51
4. If an MC D (cid:54)|= ϕ, a counterexample (CE) based on a critical subsystem can serve as diagnostic information about the source of the failure. 4. MC D (cid:54)|= φ の場合、クリティカルサブシステムに基づく反例 (CE) は、障害の原因に関する診断情報として機能する。 0.78
We consider the following CE, motivated by the notion of critical subsystem in [37]. 我々は[37]における臨界サブシステムの概念に動機づけられた次のceを考える。 0.71
Definition 4 (Counterexample). 定義4(Counterexample)。 0.74
Let D = (S, s0, P ) be an MC with s⊥ (cid:54)∈ S. The sub-MC of D induced by C ⊆ S is the MC D↓C = (S ∪ {s⊥}, s0, P (cid:48)), where the transition probability function P (cid:48) is defined by: D = (S, s0, P ) を s を持つ MC (cid:54)∈ S とする。 D の D のサブMC は、遷移確率関数 P (cid:48) が次のように定義される MC D である。 0.67
(cid:40) P (cid:48)(s) = (cid:40) P (cid:48)(s) = 0.87
P (s) [s⊥ (cid:55)→ 1] P(s) [s' (cid:55)→ 1] 0.92
if s ∈ C, otherwise. s ∈ C の場合、そうでなければ。 0.69
The set C and the sub-MC D↓C are called a counterexample (CE) for the property P≤λ[♦T ] on MC D, if D↓C (cid:54)|= P≤λ[♦(T ∩ (C ∪ {s0}))]. 集合 C と部分MC D が MC D 上の性質 P≤λ[\T ] に対して反例 (CE) と呼ばれるのは、D\C (cid:54)|= P≤λ[\(T ) (C ) {s0})] が成り立つときである。 0.80
Let Dr be an MC violating the specification ϕ. Dr を仕様 φ に違反する MC とする。 0.81
To compute other realizations violating ϕ, the oracle computes a critical subsystem Dr↓C, which is then used to deduce a so-called conflict for Dr and ϕ. Definition 5 (Conflict). φ に違反する他の実現を計算するために、oracle は重要なサブシステム dr/c を計算し、 dr と φ の定義 5 に対するいわゆる衝突を推論する。 0.76
For family of MCs D = (S, s0, K,B) and C ⊆ S, the MCs D = (S, s0, K,B) および C > S の族について、 0.72
set KC of relevant parameters (called conflict) is given by(cid:83) 関連するパラメータ(コンフリクトと呼ばれる)のKCの集合は(cid:83) 0.74
s∈C supp(B(s)). s∈C supp(B(s)) である。 0.77
Inductive Synthesis for Probabilistic Programs Reaches New Horizons 確率的プログラムのための帰納的合成 0.65
7 Fig. 2. 7 フィギュア。 2. 0.71
Counterexamples for smaller conflicts. より小さな紛争の反例。 0.68
It is straightforward to compute a set of violating realizations from a conflict. 対立による実現を侵害する一連の集合を計算するのは簡単である。 0.63
A generalization of realization r induced by the set KC ⊆ K of relevant parameters is the set r↑KC = {r(cid:48) ∈ R | ∀k ∈ KC : r(k) = r(cid:48)(k)}. 関連するパラメータの集合 KC > K によって誘導される実現 r の一般化は、集合 r = {r(cid:48) ∈ R | sk ∈ KC : r(k) = r(cid:48)(k)} である。 0.85
We often use the term conflict to refer to its generalization. conflictという用語は、その一般化を指すのによく使われる。 0.62
The size of a conflict, i.e., the number |KC| of relevant parameters KC is crucial. 競合の大きさ、すなわち、関連するパラメータ KC の数 |KC| が重要である。 0.76
Small conflicts potentially lead to generalizing r to larger subfamilies r↑KC. 小さな衝突は、r をより大きなサブファミリ r に一般化させる可能性がある。 0.48
It is thus important that the CEs contain as few parameterized transitions as possible. したがって、CEはできるだけ少ないパラメータ化遷移を含むことが重要である。 0.74
The size of a CE in terms of the number of states is not of interest. CE のサイズは、状態の数では興味がない。 0.52
Furthermore, the overhead of providing CEs should be bounded from below by the payoff: Finding a large generalization may take some time, but small generalizations should be returned quickly. さらに、cesの提供のオーバーヘッドは、大きな一般化を見つけるのにしばらくかかるかもしれないが、小さな一般化はすぐに返すべきである。 0.56
The CE-based oracle in [9] uses an off-the-shelf CE procedure [16,41], and mostly does not provide small CEs. 9]のCEベースのオラクルは、市販のCE手順[16,41]を使用し、ほとんど小さなCEを提供していません。
訳抜け防止モード: CE-based oracle in [9 ] はオフザシェルフCEプロシージャ [16,41 ] を使用する。 ほとんどは小さなCEを提供していません。
4 A Smart Oracle with Counterexamples and Abstraction 4 A Smart Oracle with Counterexamples and Abstraction 0.85
This section develops an oracle based on CEs, tailored for the use in an oracleguided inductive synthesis loop described in Sect. このセクションでは、Sect で説明されている oracleguided inductive synthesis loop の使用に合わせて、CE に基づいた oracle を開発しています。 0.65
3. Its main features are: 3. 主な特徴は次のとおりです。 0.76
– a fast greedy approach to compute CEs that provide small conflicts: We 小規模の競合を提供するCEを計算するための迅速な欲張りのアプローチ。 0.58
achieve this by taking into account the position of the parameters. パラメータの位置を考慮してこれを達成します 0.72
– awareness about the semantics of parameters by using model-checking results モデルチェック結果を用いたパラメータのセマンティクスの認識 0.65
from an abstraction of the family. 家族を抽象化したものです 0.73
Before going into details, we provide some illustrative examples. 詳しく説明する前に、いくつかの例を挙げる。 0.69
A motivating example First, we illustrate what it means to take CEs that lead to small conflicts. 動機づけの例まず、小さな紛争につながるCEを取ることの意味を説明します。 0.58
Consider Fig. 2, with a family member Dr (left), where the superscript of a state identifier si denotes parameters relevant to si. 図を考える。 状態識別子siのスーパースクリプトは、siに関連するパラメータを表す。
訳抜け防止モード: 図を考える。 2:家族のDr(左)で、そこで 状態識別子 si のスーパースクリプトは si に関連するパラメータを表す。
Consider the safety property ϕ ≡ P≤0.4[♦{t}]. 安全特性 φ {\displaystyle φ \ P≤0.4[\{t}] を考える。 0.74
Clearly, Dr (cid:54)|= ϕ, and we can construct two CEs: C1 = {s0, s3, t} (center) and C2 = {s0, s1, s2, t} (right) with conflicts KC1 = {X, Y } and KC2 = {X}, respectively. 明らかに、Dr (cid:54)|= φ であり、C1 = {s0, s3, t} (center) とC2 = {s0, s1, s2, t} (right) の2つのCEをそれぞれKC1 = {X, Y } とKC2 = {X} の競合で構成できる。 0.78
It illustrates that a smaller CE does not necessarily induce a smaller conflict. それは小さいCEが必ずしもより小さい衝突を引き起こすとは限らないことを示します。 0.58
We now illustrate awareness of the semantics of parameters. パラメータのセマンティクスの認識について説明します。 0.59
Consider the family D = (S, s0, K(cid:48),B), where S = {s0, s1, s2, t, f}, the parameters are K(cid:48) = {X, Y, T (cid:48), F (cid:48)} with domains VX = {s1, s2}, VY = {t, f}, VT (cid:48) = {t}, VF (cid:48) = {f}, and a family B of transition probability functions defined in Fig. ファミリ D = (S, s0, K(cid:48),B), ここで S = {s0, s1, s2, t, f}, パラメータは K(cid:48) = {X, Y, T(cid:48), F(cid:48)} であり、領域 VX = {s1, s2}, VY = {t, f}, VT(cid:48) = {t}, VF(cid:48) = {f} であり、Fig で定義される遷移確率関数のファミリ B である。 0.89
3 (left). As the 3位(左)。 として 0.78
0.50.510.50.510.50.5 0.50.510.50.510.50.5 0.50.510.50.510.50.5 0.50.510.50.510.50.5 0.50.510.50.510.50.5 0.50.510.50.510.50.5 0.06
8 R. Andriushchenko et al. 8 r. andriushchenkoら。 0.77
B(s0) = [X (cid:55)→ 1], B(s1) = [T B(s2) = [T B(t) = [T B(f ) = [F B(s0) = [X (cid:55)→ 1], B(s1) = [T B(s2) = [T B(t) = [T B(f ) = [F] 0.94
(cid:48) (cid:55)→ 0.6, Y (cid:55)→ 0.2, F (cid:48) (cid:55)→ 0.2, Y (cid:55)→ 0.2, F (cid:48) (cid:55)→ 1], (cid:48) (cid:55)→ 1] (cid:48)→ 0.6, Y (cid:55)→ 0.2, F (cid:48)→ 0.2, Y (cid:55)→ 0.2, F (cid:48) (cid:55)→ 1], (cid:48)→ 1] 0.93
(cid:48) (cid:55)→ 0.2], (cid:48) (cid:55)→ 0.6], (cid:48) (cid:55)→ 0.2], (cid:48) (cid:55)→ 0.6], 0.80
Fig. 3. A family D of four Markov chains (unreachable states are grayed out). フィギュア。 3. 4つのマルコフ鎖のファミリーD(到達不能状態はグレーアウトされる)。 0.65
parameters T (cid:48) and F (cid:48) each can take only one value, we consider K = {X, Y } as the set of parameters. パラメータ T (cid:48) と F (cid:48) はそれぞれ1つの値のみを取ることができ、K = {X, Y } をパラメータの集合とみなす。 0.84
There are |VX| × |VY | = 4 family members, depicted in Fig. VX| × |VY | = 4家族がおり、図1に描かれている。 0.72
3(right). For conciseness, we omit some of the transition probabilities (recall that transition probabilities sum to one). 3(右)。 簡潔性のために、遷移確率のいくつかを省略する(遷移確率は 1 に等しい)。 0.69
Only realization r3 satisfies the safety property ϕ ≡ P≤0.3[♦{t}]. 唯一の実現 r3 は安全特性 φ {\displaystyle φ \ P≤0.3[\{t}] を満たす。 0.69
CEGIS [9] illustrated : Consider running CEGIS, and assume the oracle gets realization r0 first. CEGIS [9] を例示します: CEGIS を実行し、オラクルが最初に r0 を実現すると仮定します。 0.67
A model checker reveals P[Dr0, s0 |= ♦T ] = 0.8 > 0.3. モデルチェッカーは、p[dr0, s0 |= st ] = 0.8 > 0.3 を示す。 0.68
The CE for Dr0 and ϕ contains the (only) path to the target: s0→s1→ t having probability 0.8 > 0.3. Dr0 と φ の CE は対象への(唯一の)経路を含む: s0→s1→ t は確率 0.8 > 0.3 である。 0.72
The corresponding CE C = {s0, s1, t} induces the conflict KC = {X, Y }. 対応するCE C = {s0, s1, t} は競合 KC = {X, Y } を誘導する。 0.79
None of the parameters is generalized. いずれのパラメータも一般化されない。 0.69
The same argument applies to any subsequent realization: the constructed CEs do not allow for generalization, the oracle returns only the passed realization, and the learner keeps iterating until accidentally guessing r3. 構築されたcesは一般化を許可せず、oracleはパスされた実現のみを返却し、学習者は偶然r3を推測するまで反復を続ける。 0.64
Can we do better? より良くできるでしょうか? 0.77
To answer this, consider CE generation as a game: The Pruner creates a critical subsystem C. The Adversary wins if it finds a MC satisfying ϕ containing C, thus refuting that C is a counterexample. The Pruner create a critical subsystem C; The Adversary wins if it finding MC fulfilling φ containing C, so disfuting that C is a counterexample。
訳抜け防止モード: これに対する答えとして、CE生成をゲームとして考えてみましょう。 The Adversary wins if it find a MC fulfilling φ containing C, したがって、C は反例である。
In our setting, we change the game: The Adversary must select a family member rather than an arbitrary MC. 我々の設定では、ゲームを変更する: 管理者は任意のMCではなく、家族を選ばなければならない。
訳抜け防止モード: 私たちの設定では、私たちはゲームを変えます The Adversary must select a family than a arbitrary MC。
Analogously, off-the-shelf CE generators construct a critical subsystem C that for every possible extension of C is a CE. 同様に、既製のCEジェネレータは、Cのあらゆる拡張がCEである重要なサブシステムCを構築する。 0.73
These are CEs without context. これらはコンテキストのないCEです。 0.62
In our game, the Adversary may not extend the MC arbitrarily, but must choose a family member. 我々のゲームでは、敵対者はMCを任意に拡張することはできないが、家族を選ばなければならない。 0.58
These are CEs modulo a family. これらはCEs modulo a familyである。 0.73
Back to the example: Observe that for a CE for Dr0, we could omit states t and s1 from the set C of critical states: we know for sure that, once Dr0 takes transition (s0, s1), it will reach target state t with probability at least 0.6. 例に戻すと: ce for dr0 に対して、臨界状態の集合 c から t と s1 を省略することができる: dr0 が遷移すると(s0, s1)、少なくとも 0.6 の確率で目標状態 t に到達することが確実に分かっている。 0.81
This exceeds the threshold 0.3, regardless of the value of the parameter Y . これはパラメータ y の値に関係なくしきい値 0.3 を超える。 0.85
Hence, for family D, the set C(cid:48) = {s0} is a critical subsystem. したがって、ファミリー D の場合、集合 C(cid:48) = {s0} は重要なサブシステムである。 0.75
The immediate advantage is that this set induces conflict KC(cid:48) = {X} (parameter Y has been generalized). 直接的な利点は、この集合が競合 KC(cid:48) = {X} を引き起こすことである(パラメータ Y は一般化されている)。 0.58
This enables us to reject all realizations from the set r0↑KC(cid:48) = {r0, r1}. これにより、集合 r0\kc(cid:48) = {r0, r1} からすべての実現を拒絶することができる。 0.60
It is ‘easier’ to construct a CE for a (sub)family than for arbitrary MCs. 任意のMCよりも(サブ)ファミリーのためのCEを構築するのは「簡単」です。 0.67
More generally, a successful oracle needs to have access to useful bounds, and effectively integrate them in the CE generation. より一般的には、成功したオラクルは有用な境界にアクセスでき、CE世代に効果的に統合する必要がある。 0.62 60.2 60.2 0.13
Inductive Synthesis for Probabilistic Programs Reaches New Horizons 確率的プログラムのための帰納的合成 0.65
9 Counterexample construction We develop an algorithm using bounds on reachability probabilities, similar to the bounds used above. 9 対例構造 上記の境界と同様、到達可能性確率の境界を用いたアルゴリズムを開発しています。 0.78
Let us assume that for some set of realizations R and for every state s, we have bounds lb R (s), ub (s), such that for every r ∈ R we have lb (s) ≤ P[Dr, s |= ♦T ] ≤ ub R R (s). ある実化 R の集合とすべての状態 s に対して、すべての r ∈ R に対して lb (s) ≤ P[Dr, s |= s T ] ≤ ub R (s) を満たすような有界 lb R (s, ub (s) を持つと仮定する。 0.81
Such bounds always exist (take 0 and 1). そのような境界は常に存在する (take 0 と 1)。 0.68
We see later how we compute these bounds. これらの境界を計算する方法は後述する。 0.56
In what follows, we fix r and denote Dr = (S, s0, P ). 次の例では r を固定し、Dr = (S, s0, P ) と表す。 0.67
Let us assume Dr violates a safety property ϕ ≡ P≤λ[♦T ]. Dr が安全性 φ {\displaystyle φ} に反すると仮定する。 0.66
The following definition is central: Definition 6 (Rerouting). 次の定義は中心的なものです:定義6(ルーティング)。 0.73
Let MC D = (S, s0, P ) with s(cid:62), s⊥ (cid:54)∈ S, C ⊆ S a set of expanded states and γ : S \ C → [0, 1] a rerouting vector. MC D = (S, s0, P ) を s (cid:62), s , (cid:54)∂ S, C , S を拡張状態の集合とし、γ : S \ C → [0, 1] を再帰ベクトルとする。 0.91
The rerouting of MC D w.r.t. MC D w.r.t。 0.62
C and γ is the MC D↓C[γ] = (S ∪ {s⊥, s(cid:62)}, s0, P C C と γ は MC D*C[γ] = (S ) {s , s(cid:62)}, s0, P C である。 0.95
R γ ) with: R γ ) with: 0.85
P (s) P (複数形 Ps) 0.58
P C γ (s) = P C γ (s) = 0.85
[s(cid:62) (cid:55)→ γ(s), s⊥ (cid:55)→ (1−γ(s))] [s (cid:55)→ 1] [s(cid:62) (cid:55)→γ(s), s (cid:55)→ (1−γ(s))] [s (cid:55)→ 1] 0.98
if s ∈ C, if s ∈ S\C, if s ∈ {s(cid:62), s⊥}. s ∈ C ならば s ∈ S\C ならば s ∈ {s(cid:62), s\} である。 0.93
Essentially, D↓C[γ] extends the MC D with additional sink states s(cid:62) and s⊥ and replaces all outgoing transitions of any non-expanded state s ∈ S\C by a transition leading to s(cid:62) (with probability γ(s)) and a complementary one to s⊥. 本質的に、d\c[γ] はmc d を追加のシンク状態 s(cid:62) と s\ で拡張し、任意の非拡大状態 s ∈ s\c のすべての出力遷移を s(cid:62) への遷移(確率 γ(s)) と s への相補的な遷移に置き換える。 0.75
We consider s(cid:62) to be the new target and let ϕ(cid:48) denote the updated property. s(cid:62) を新しい対象とし、 φ(cid:48) を更新されたプロパティとする。 0.71
The γ(s)−−−→ s(cid:62) may be considered a ‘shortcut’ that by-passes successors of transition s s and leads straight to target s(cid:62) with probability γ(s). γ(s)−−−−→ s(cid:62) は遷移 s の後継を通り、確率 γ(s) でターゲット s(cid:62) に直結する「ショートカット」と見なすことができる。 0.79
To ensure that D↓C[γ] is a CE, the value γ(s) must be a lower bound on the reachability probability from s in D. When constructing a CE for a singular MC, we pick γ = 0, whereas when this MC is induced by a realization r ∈ R, we can safely pick γ = lb R . 特異な MC に対して CE を構築するとき、我々は γ = 0 を選ぶが、この MC が実化 r ∈ R によって誘導されるとき、安全に γ = lb R を選択することができる。
訳抜け防止モード: c[γ ] が ce であることを保証するためには、特異な mc に対して ce を構成するとき、値 γ(s ) は d 内の s から到達可能性確率に対して下限でなければならない。 γ = 0 を選ぶと このmcは実数化 r ∈ r によって誘導される。 γ = lb r を安全に選べる。
The CE will be valid for every r(cid:48) ∈ R. It is a CE-modulo-R. Algorithmically, we employ a state-exploration approach and therefore start with C (0) = ∅, i.e., all states are initially rerouted. CE はすべての r(cid:48) ∈ R に対して有効である。CE-modulo-R である。
訳抜け防止モード: CE はすべての r(cid:48 ) ∈ R に対して有効である。 私たちは状態-探索アプローチを採用しており、C(0) = ^ で始まります。 すなわち すべての州は 当初 取り消されてしまった
If this is a CE, we are done. これがCEであれば、私たちは完了です。 0.67
Otherwise, if the rerouting D↓C (0)[γ] satisfies ϕ(cid:48), then we ‘expand’ some states to obtain a CE. さもなくば、再帰的 D = C (0)[γ] が φ(cid:48) を満たすなら、CE を得るためにいくつかの状態を拡張する。 0.65
Naturally, we must expand reachable states to change the satisfaction of ϕ. 当然、我々はφの満足度を変えるために到達可能な状態を拡張する必要がある。 0.61
By expanding some state s ∈ S, we abandon the abstraction γ(s)−−−→ s(cid:62) and replace it with concrete behavior that associated with the shortcut s was inherent to state s in MC D. Expanding a state cannot decrease the induced R reachability probability as lb is a valid lower bound. ある状態 s ∈ S を拡大することによって、抽象 γ(s)−−→ s(cid:62) を放棄し、ショートカット s が MC D における状態 s に固有の具体的な挙動に置き換える。
訳抜け防止モード: いくつかの状態 s ∈ S を拡張することにより、抽象的 γ(s)−−−−→ s(cid:62 ) を放棄する。 具体的行動に置き換わり ショートカット s は MC D の状態 s に固有のものである。 lb が有理下界であるので、誘導された R の到達確率を下げることはできない。
This gradual expansion of the reachable state space continues until for some C ⊆ S the corresponding rerouting D↓C[γ] violates ϕ(cid:48). 到達可能な状態空間のこの段階的拡大は、ある C > S に対して対応する再帰 D > C[γ] が φ(cid:48) に反するまで続く。 0.63
This gradual expansion process terminates as D↓S[γ] ≡ D and our assumption is D (cid:54)|= ϕ. この漸進展開過程は d を d として終了し、我々の仮定は d (cid:54)|= φ である。 0.75
We show this process on an example. このプロセスを例に示します。 0.69
Example 1. Reconsider D in Fig. 例1。 図Dを再考する。 0.70
3 with ϕ ≡ P≤0.3[♦{t}]. 3 の φ は P≤0.3[\{t}] である。 0.86
Using the method = [s0 (cid:55)→ 0.2, s1 (cid:55)→ 0.6, s2 (cid:55)→ 0.2, t (cid:55)→ 1, f (cid:55)→ 0]. s0 (cid:55)→ 0.2, s1 (cid:55)→ 0.6, s2 (cid:55)→ 0.2, t (cid:55)→ 1, f (cid:55)→ 0] を用いる。 0.80
In outlined below we get: lb absence of any bounds, the CE is {s0, s1, t}. 以下に概説する: lb 任意の境界が存在しないとき、CE は {s0, s1, t} である。 0.67
Consider the gradual rerouting , C (0) = ∅ and have D(0) := Dr0↓C (0)[γ], see Fig. 段階的再ルーティング , C (0) = ^ を考えると、D(0) := Dr0*C (0)[γ] は Fig を参照のこと。 0.82
4(a). approach: We set γ = lb Verifying this MC against ϕ(cid:48) = P≤0.3[♦T ∪{s(cid:62)}] yields P[D(0), s0 |= ♦T ∪{s(cid:62)}] = γ(s0) = 0.2 ≤ 0.3, i.e., the set C (0) is not a CE. 4(a)。 アプローチ: このMC に対して γ = lb を φ(cid:48) = P≤0.3[>T >{s(cid:62)}] とすると P[D(0), s0 |= >T >{s(cid:62)}] = γ(s0) = 0.2 ≤ 0.3,すなわち集合 C(0) は CE ではない。 0.83
We now expand the initial state, i.e., C (1) = {s0} and let D(1) := Dr0↓C (1)[γ], see Fig. 次に、初期状態、すなわち C (1) = {s0} を拡張し、D(1) := Dr0*C (1)[γ] を Fig で表す。 0.79
4(b). Verifying D(1) yields P[D(1), s0 |= ♦T ∪ {s(cid:62)}] = 1 · γ(s1) = 0.6 > 0.3. 4(b)。 D(1) の検証は P[D(1), s0 |= sT ^ {s(cid:62)}] = 1 · γ(s1) = 0.6 > 0.3 となる。 0.84
Thus, the set C (1) is critical したがって、集合 c(1) は臨界である 0.81
R R R R 0.85
10 R. Andriushchenko et al. 10 r. andriushchenkoら。 0.77
Fig. 4. Finding a CE to Dr0 and ϕ from Fig. フィギュア。 4. Fig から CE から Dr0 と φ を見つける。 0.69
3 using the rerouting vector γ = lbR. 3 再ルーティングベクトル γ = lbR を用いる。 0.86
Algorithm 1: Counterexample construction based on rerouting. アルゴリズム1:再ルーティングに基づく反例構築。 0.75
: An MC Dr a property ϕ ≡ P(cid:46)(cid:47)λ[♦T ] s.t. : MC Dr a property φ ^ P(cid:46)(cid:47)λ[*T ] s.t。 0.90
Dr (cid:54)|= ϕ, a rerouting vector γ. Dr (cid:54)|= φ, a rerouting vector γ。 0.92
Input Output : A conflict K for Dr and ϕ. 入力出力 : Dr と φ の競合 K。 0.67
1 i ← 0, K (i) ← ∅ 2 while true do 3 1 i > 0, K (i) > > 2 であり、真は do 3 である。 0.65
5 4 C (i), H (i) ← reachableViaHoles(Dr , K (i)) D(i) ← Dr↓C (i)[γ] if P[D(i) |= ♦T ∪ {s(cid:62)}] (cid:54)(cid:46)(cid :47) λ then return K (i); s ← chooseToExpand(H (i), K (i)) K (i+1) = K (i) ∪ supp(B(s)) i ← i + 1 8 9 end while 5 4 C (i), H (i) ・ reachableViaHoles(Dr , K (i)) D(i) ・ Dr ・ C (i)[γ] if P[D(i) |= ・ T ・ {s(cid:62)}] (cid:54)(cid:46)(cid :47) λ then return K (i); s ・ chooseToExpand(H (i), K (i)) K (i+1) = K (i) ・ supp(B(s))) i ・ i + 1 8 9 end while 0.85
6 7 and the corresponding conflict is KC(1) = supp(s0) = {X}. 6 7 対応する競合は KC(1) = supp(s0) = {X} である。 0.82
This is smaller than the naively computed conflict {X, Y }. これは、naively computed conflict {x, y } よりも小さい。 0.77
Greedy state expansion strategy Recall from Fig. グレーディ州の拡張戦略 図からリコールします。 0.52
2 that for an MC Dr with Dr (cid:54)|= ϕ, multiple CEs may exist inducing different conflicts. 2 MC Dr with Dr (cid:54)|= φ の場合、複数のCEが異なる競合を引き起こす可能性がある。 0.75
An efficient expansion strategy should yield a CE that induces a small amount of relevant parameters (to prune more family members) and this CE is preferably obtained by a small number of model-checking queries. 効率的な拡張戦略は、少数の関連するパラメータ(より多くの家族をプルーする)を誘導するCEを生成し、このCEは、少数のモデルチェッククエリによって得られることが好ましい。 0.67
The method presented in Alg. Algで示される方法。 0.60
1 meets these criteria. 1はこれらの基準を満たす。 0.55
The algorithm expands multiple states between subsequent model checks, while expanding only states that are associated with parameters that are relevant. このアルゴリズムは、その後のモデルチェック間で複数の状態を拡張する一方で、関連するパラメータに関連する状態のみを拡張する。 0.73
In particular, in each iteration, we keep track of the set K (i) of relevant parameters optimistically starting with K (0) = ∅. 特に、各反復において、K (0) = ... から楽観的に始まる関連するパラメータの集合 K (i) をトラックする。 0.70
We compute (see line 3) the set C (i) of states that are reachable from the initial state via states which are associated only with relevant parameters in K (i), i.e., via states for which supp(B(s)) ⊆ K (i). 我々は、初期状態から到達可能な状態の集合 C(i) を、K(i) 内の関連するパラメータのみに関連付けられた状態、すなわち、Supp(B(s)) > K(i) を経由する状態によって計算する(ライン3参照)。 0.78
Here, H (i) represents a state exploration ‘horizon’: the set of states reachable from C (i) but containing some (still) irrelevant parameters. ここで H (i) は状態探索の「水平」を表す: C (i) から到達可能な状態の集合だが、(まだ)無関係なパラメータを含む。 0.81
We then construct the corresponding rerouting D↓C (i)[γ] and check whether it is a CE. 次に、対応する再帰的 D\C (i)[γ] を構築し、それが CE であるかどうかを確認する。 0.65
Otherwise, we greedily choose a state s from the horizon H (i) containing the least number of irrelevant parameters and add these parameters to our conflict (see line 7). そうでなければ、最小数の無関係なパラメータを含む水平線 H (i) から状態 s を選択し、これらのパラメータを衝突に追加します(ライン7参照)。 0.74
10.8110. 0.41110.8110.20.6110 .411 10.8110. 0.41110.8110.20.6110 .411 0.11
Inductive Synthesis for Probabilistic Programs Reaches New Horizons 確率的プログラムのための帰納的合成 0.65
11 D, Φ Abstr-Oracle 11 d, φ Abstr-Oracle 0.67
R(cid:48) ⊆ R R(cid:48) = R 0.87
r ∈ R+bounds r ∈ R+bounds 0.78
R each r ∈ R(cid:48), r |= Φ R 各 r ∈ R(cid:48), r |= s 0.90
bounds or R(cid:48) violates 境界またはR(cid:48)が違反する 0.57
Learner no r |= Φ 学習者 なし r |= φ 0.70
R(cid:48) ⊆ R violate Φ R(cid:48) Rは違反する。 0.75
D, Φ CE-Oracle d, φ CE-Oracle 0.58
r |= Φ Fig. r |= 。 フィギュア。 0.65
5. Conceptual hybrid (dual-oracle) synthesis 5. 概念ハイブリッド(デュアルオラクル)合成 0.85
. The resulting conflict may not be minimal, but is computed fast. . 結果として生じる競合は最小限ではなく、高速に計算される。 0.70
Our algorithm applies to probabilistic liveness properties2 too using γ = ub このアルゴリズムはγ = ub を用いて確率的生存特性2にも適用できる。 0.64
R . Computing bounds We compute lb using an abstraction [10]. R . 計算境界 lb を抽象 [10] を使って計算する。 0.82
The method considers some set R of realizations and computes the corresponding quotient Markov decision process (MDP) that over-approximates the behavior of all MCs in the family R. Model checking this MDP yields an upper and a lower bound of the induced probabilities for all states over all realizations in R. That is, Bound(D,R) computes lb この手法は、いくつかの実現の集合 R を考慮し、対応する商マルコフ決定過程 (MDP) を、ファミリー R 内のすべての MC の振る舞いを過近似に計算する。この MDP をチェックするモデルでは、R のすべての実現上のすべての状態に対する誘導確率の上限と下限が与えられる。 0.84
and ub R R そしてubは R R 0.81
R lb (s) ≤ min r∈R R lb (s) ≤ min r∈R 0.87
R ∈ RS and ub P[Dr, s |= ♦T ] ≤ max r∈R R ∈ RS と ub P[Dr, s |= yT ] ≤ max r∈R 0.99
R ∈ RS such that for each s ∈ S: P[Dr, s |= ♦T ] ≤ ub R R ∈ RS は各 s ∈ S に対して P[Dr, s |= sT ] ≤ ub R となる。 0.94
(s). To allow for refinement, two properties are crucial (with point-wise inequalities): (s)。 精緻化を可能にするには、2つの特性が重要です(ポイントワイズ不等式)。 0.64
1. lb R ≤ lb 1. lb R ≤ lb 0.87
R(cid:48) ∧ ub R(cid:48) = ub 0.84
R ≥ ub R(cid:48) R ≥ ub R(cid:48) 0.85
for R(cid:48) ⊆ R and 2. lb R(cid:48) > R と 2. lb について 0.69
{r} {r} = ub {r} {r} =ub 0.82
for r ∈ R. r ∈ R に対して。 0.80
In [10], the abstraction and refinement together define an abstraction-refinement loop (AR) that addresses the feasibility problem. 10]では、抽象化と洗練が一緒に実現可能性問題に対処する抽象化・リファインメントループ(AR)を定義します。 0.67
In the worst case, this loop analyses 2 · |R| quotient MDPs, which (as of now) may be arbitrarily larger than the number of family members they represent. 最悪の場合、このループは2 · |R| 商 MDP を分析し、(現在のところ)彼らが表す家族数よりも任意に大きいかもしれない。 0.78
5 Hybrid Dual-Oracle Synthesis 5 ハイブリッドデュアルOracle合成 0.87
We introduce an extended synthesis loop in which the abstraction-based reasoning is used to prune the family R, and to accelerate the CE-based oracle from Sect. 本研究では, 抽象に基づく推論を用いて, ファミリーRをプルーニングし, セクトからセリウムベースのオーラクルを加速する拡張合成ループを提案する。 0.71
4. The intuitive idea is outlined in Fig. 4. 直感的なアイデアは図で概説されている。 0.71
5. Note that if the CE-based oracle is not exploited, we emulate AR (explained in computing bounds above), whereas if the abstraction oracle is not used, we emulate CEGIS (with the novel oracle). 5. CEベースのオラクルが利用されない場合、ARをエミュレートする(上述の計算境界で説明される)のに対し、抽象化のオラクルを使わない場合は、CEGISをエミュレートする(新しいオラクルで)。 0.80
Let us motivate combining these oracles in a flexible way. これらのオラクルを柔軟に組み合わせる動機付けをしましょう。 0.52
The naive version outlined in the previous section assumed a single abstraction step, and invokes CEGIS with the bounds obtained from that step. 前節で概説したナイーブバージョンは、単一の抽象化ステップを仮定し、そのステップから得られたバウンダリでCEGISを起動する。 0.65
Evidently, the better (tighter) the bounds γ, the better the CEs. 明らかに、境界 γ がより良く(より高くなる)ほど、CE はより良くなる。 0.63
However, the abstraction-based bounds for R may be very loose. しかし、R の抽象的境界は非常に緩いかもしれない。 0.66
These bounds can be improved by splitting the set R and using the bounds on the two sub-families. これらの境界は、集合 R を分割し、2 つのサブファミリー上の境界を使用することで改善することができる。
訳抜け防止モード: これらの境界は改善できる 集合 R を分割し、2つのサブファミリーのバウンダリを使用する。
The idea is to run a limited number of そのアイデアは、限られた数を実行することです 0.62
2 Some care is required regarding loops, see [9]. 2 ループに注意が必要です。 [9] を参照してください。 0.69
12 R. Andriushchenko et al. 12 r. andriushchenkoら。 0.77
Algorithm 2: Hybrid (dual-oracle) synthesis. アルゴリズム2:ハイブリッド(デュアルオーラクル)合成。 0.75
: A family D, a reachability property ϕ. A family D, a reachability property φ。 0.64
Input Output : Either a member r in D with r |= ϕ, or no such r exists in D 入力出力 : D のメンバ r が r |= φ を持つか、あるいはそのような r が D に存在しないか。
訳抜け防止モード: 入力出力 : r |= φ を持つ D のメンバ r か あるいは D にそのような r は存在しない
// each analysed (sub-)family also holds bounds // time allocation factor for CEGIS 各分析対象(サブ)ファミリーもCEGISの境界//時間割り当て係数を保持します。 0.67
5 4 1 R ← {RD} ; 2 δCEGIS ← 1 ; 3 while true do result,R(cid:48) , σAR, tAR ←AR.run(R, ϕ) if result.decided() then return result; CEGIS.setTimeout(tAR · δCEGIS) result, σCEGIS,R(cid:48)(cid: 48) ← CEGIS.run(R(cid:48) , ϕ) if result.decided() then return result; δCEGIS ← σCEGIS/σAR R ← R(cid:48)(cid:48) 10 11 end while 5 4 σIS.setTimeout(tAR · δCEGIS) result, σCEGIS, R(cid:48)(cid:48)(ci d:48) , φ) if result.decided() then return result; CEGIS.setTimeout(tAR · δCEGIS) result, σCEGIS, R(cid:48)(cid:48) , φ) if result.decided() then return result; δGIS > σCEGIS/σAR R > R(cid:48) 10 end end 0.81
6 7 8 9 AR steps and then invoke CEGIS. 6 7 8 9 ARステップとCEGISを呼び出します。 0.84
Our experiments reveal that it can be crucial to be adaptive, i.e., the integrated method must be able to detect at run time when to switch. 私たちの実験では、適応性、すなわち、統合メソッドは、切り替える時に実行時に検出できることが重要であることが明らかになった。 0.70
The proposed hybrid method switches between AR and CEGIS, where we allow for refining during the AR phase and use the obtained refined bounds during CEGIS. 提案されたハイブリッド手法はARとCEGISを切り替え、ARフェーズ中に精製し、CEGIS中に得られた精製境界を使用する。 0.66
Additionally, we estimate the efficiency σ (e.g., the number of pruned MCs per time unit) of the two methods and allocate more time t to the method with superior performance. さらに, 2つの手法の効率σ(例えば時間単位あたりのpruned MCの数)を推定し, 優れた性能を有する手法により多くの時間tを割り当てる。 0.79
That is, if we detect that CEGIS prunes sub-families twice as fast as AR, we double the time in the next round for CEGIS. すなわち、CEGISがARの2倍の速さでサブファミリを産むことを検知した場合、CEGISの次のラウンドで2倍の時間を費やす。 0.68
The resulting algorithm is summarized in Alg. 結果のアルゴリズムはalgで要約される。 0.72
2. Recall that AR (at line 5) takes one family from R, either solves it or splits it and returns the set of undecided families R(cid:48) . 2. AR(5行目)がRから1つのファミリーを取り、それを解くか分割し、未決定のR(cid:48)の集合を返すことを思い出す。 0.81
In contrast, CEGIS processes multiple families from R(cid:48) . 対照的に、CEGISはR(cid:48)から複数のファミリーを処理する。 0.60
This workflow is motivated by the fact that one iteration of AR (i.e., the involved MDP model-checking) is typically significantly slower that one CEGIS iteration. このワークフローは、1つのAR(つまり、関連するMDPモデルチェック)が1つのCEGISイテレーションよりもかなり遅いという事実によって動機付けられている。 0.64
until the timeout and then returns the set of undecided families R(cid:48)(cid:48) タイムアウトまで、そして未決定の族R(cid:48)(cid:48)の集合を返す 0.70
Remark 1. Although the developed framework for integrated synthesis has been discussed in the context of feasibility with respect to a single property ϕ, it can be easily generalized to handle multiple-property specifications as well as to treat optimal synthesis. 備考1。 単一性質φに対する実現可能性の文脈で、統合合成のための開発されたフレームワークが議論されているが、マルチプロパティ仕様を扱うだけでなく、最適な合成を扱うために容易に一般化することができる。 0.60
Regarding multiple properties, the idea remains the same: Analyzing the quotient MDP with respect to multiple properties yields multiple probability bounds. 複数の性質に関しても、この考えは同じである:複数の性質に関して商 MDP を分析すると、複数の確率境界が得られる。 0.63
After initiating a CEGIS-loop and obtaining an unsatisfiable realization, we can construct a separate conflict for each unsatisfied property, while using the corresponding probability bound to enhance the CE generation process. CEGISループを起動し、不満足な実現を得た後、CE生成プロセスを強化するために対応する確率を用いて、各不満足な特性に対して別々の競合を構築することができる。 0.62
Optimal synthesis is handled similarly to feasibility, but, after obtaining a satisfiable solution, we update the optimizing property to exclude this solution: e.g., for maximal synthesis this translates to increasing the threshold of the maximizing property. 最適合成は実現可能性と同様に扱われるが、満足可能な解を得た後、この解を除外するために最適化特性を更新する。
訳抜け防止モード: 最適な合成が可能です。 しかし、満足のいく解決策を得た後、このソリューションを排除するために最適化プロパティを更新します。 例えば、最大合成の場合、これは最大化特性のしきい値の増加につながります。
Having exhausted the search space of family members, the last obtained solution is declared to be the optimal one. 家族のメンバーの検索スペースを枯渇させた後、最後に得られたソリューションは最適なソリューションであると宣言されます。 0.63
Inductive Synthesis for Probabilistic Programs Reaches New Horizons 確率的プログラムのための帰納的合成 0.65
13 model |K| |RD| MDP size avg. 13 モデル |K| |RD| MDP size avg。 0.79
MC size 65k Grid Maze 20 1M 9k DPM 16 43M 9.5k MCサイズ65kグリッド迷路 201M 9k DPM 16 43M 9.5k 0.72
1.2k 5.4k 2.2k 1.2k 5.4k 2.2k 0.36
8 11.5k |K| |RD| MDP size avg. 8 11.5k |K| |RD| MDP size avg。 0.68
MC size model Pole 17 1.3M 6.6k 48k Herman 8 0.5k Herman∗ 7 3.1M 6k MCサイズモデル Pole 17.3M 6.6k 48k Herman 8 0.5k Herman∗ 7 3.1M 6k 0.61
5.6k 5.2k 1k 5.6k 5.2k 1k 0.43
Table 1. Summary of the benchmarks and their statistics 表1。 ベンチマークの概要と統計 0.66
6 Experimental evaluation Implementation. 6 実験的評価 実装。 0.73
We implemented the hybrid oracle on top of the probabilistic model checker Storm [18]. 確率論的モデルチェッカーStorm[18]上にハイブリッドオラクルを実装した。 0.63
While the high-performance parts were implemented in C++, we used a python API to flexibly construct the overall synthesis loop. 高性能部品はC++で実装されましたが、python APIを使用して総合合成ループを柔軟に構築しました。 0.64
For SMT solving, we used Z3 [29]. SMTの問題解決にはZ3[29]を使用しました。 0.60
The tool chain takes a PRISM [27] or JANI [6] sketch and a set of temporal properties, and returns a satisfying realization, if such exists, or outputs that such realization does not exist. ツールチェーンは、PRISM[27]またはJANI[6]スケッチと時間特性のセットを取り、そのような場合、満足のいく実現、またはそのような実現が存在しない出力を返します。 0.74
The implementation in the form of an artefact is available at https://zenodo.org/r ecord/4422543. artefact形式の実装は、https://zenodo.org/r ecord/4422543で利用可能である。 0.63
Set-up. We compare the adaptive oracle-guided synthesis with two state-of-the-art synthesis methods: program-level CEGIS [9] using a MaxSat CE generation [16,41] and AR [10]. セットアップ。 適応オラクル誘導合成法と, MaxSat CE 生成 [16,41] と AR [10] を用いたプログラムレベル CEGIS [9] の2つの最先端合成法を比較した。 0.74
These use the same architecture and data structures from Storm. これらはstormと同じアーキテクチャとデータ構造を使っている。 0.71
All experiments are run on an Ubuntu 19.04 machine with Intel i5-8300H (4 cores at 2.3 GHz) and using up to 8 GB RAM, with all the algorithms being executed on a single thread. すべての実験は、Intel i5-8300H(2.3GHzの4コア)と最大8GBのRAMを搭載したUbuntu 19.04マシン上で実行され、全てのアルゴリズムは1スレッドで実行される。 0.76
The benchmarks consists of five different models, see Table 1, from various domains that were used in [9,10]. ベンチマークは,[9,10]で使用されたさまざまなドメインのテーブル1を参照して,5つの異なるモデルで構成されている。 0.67
As opposed to the benchmark considered in [9,10], we use larger variants of Grid and Herman to better demonstrate differences in the performance of individual methods. 9,10]で検討されたベンチマークとは対照的に、個々のメソッドのパフォーマンスの違いをよりよく示すために、GridとHermanの大きなバリエーションを使用します。
訳抜け防止モード: 9,10 ] で考慮されるベンチマークとは対照的に グリッドとハーマンの大きな変種を使い 個々の方法の性能の相違をよりよく示す。
To investigate the scalability of the methods, we consider a new variant of the Herman model, that allows us to scale the number of randomization strategies and thus the family size. 提案手法のスケーラビリティを検討するために,ランダム化戦略の数と家族の大きさをスケールできるhermanモデルの新しい変種について検討する。 0.71
In particular, we will compare performance on two instances of different sizes: small Herman∗ (5k members) and large Herman∗ (3.1M members, other statistics are reported in Table 1). 特に、サイズが異なる2つのインスタンスのパフォーマンスを比較する: small herman∗ (5k member) と large herman∗ (3.1m member, other statistics are reporting in table 1) である。 0.73
To reason about the pruning efficiency of different synthesis methods, we want to avoid feasible synthesis problems, where the order of family exploration can lead to inconsistent performance. 異なる合成方法の刈り取り効率を判断するために,家族探索の順序が一貫性のない性能につながるような,実現可能な合成問題を避けたい。 0.79
Instead, we will primarily focus on nonfeasible problems, where all realizations need to be explored in order to prove unsatisfiability. 代わりに、私たちは主に、不満足を証明するためにすべての実現を探求する必要がある、実現不可能な問題に焦点を合わせます。 0.54
The experimental evaluation is presented in three parts. 実験的な評価は3つにまとめられる。 0.74
(1) We evaluate the novel CE construction method and compare it with the MaxSat-based oracle from [9]. 1) 新規なCE構築法を評価し, [9] の MaxSat に基づくオラクルと比較した。 0.72
(2) We compare the hybrid synthesis loop with the two baselines AR and CEGIS. 2) ハイブリッド合成ループと2つのベースラインARとCEGISを比較します。 0.74
(3) We consider novel hard synthesis instances (multi-property synthesis, finding optimal programs) on instances of the model Herman∗. (3) モデルエルマンシュのインスタンス上での新しいハード合成インスタンス(マルチプロパティ合成、最適なプログラムを見つける)を検討する。 0.69
Comparing CE construction methods We consider the quality of the CEs and their generation time. CE構築法の比較では,CEの品質と生成時間について考察する。 0.81
In particular, we want to investigate (1) whether using CEs-modulo-families yields better CEes, (2) how the quality of CEs from the smart oracle compares to the MaxSat-based oracle, and how their time consumption compares. 特に,(1)CEs-modulo-famil iesの使用によりCEが向上するか否か,(2)スマートオラクルのCEの品質がMaxSatベースのオラクルとどのように比較され,その時間消費が比較されるかを検討する。 0.74
As a measure of quality of a CE, the average number of its relevant parameters w.r.t. CEの品質の尺度として、関連するパラメータの平均数w.r.t。 0.79
the total number of its parameters is taken. そのパラメータの合計数は取られる。 0.68
That is, smaller つまり、小さいです。 0.78
14 R. Andriushchenko et al. 14 r. andriushchenkoら。 0.77
model MaxSat [16] モデル MaxSat [16] 0.81
Grid Maze DPM グリッド 迷路 DPM 0.66
Pole Herman 0.59 (0.025) 0.50 (0.001) ∗ 0.74 (0.026) 0.65 (0.001) 0.21 (0.247) 0.55 (0.009) ∗ 0.24 (2.595) 0.63 (0.012) 0.32 (0.447) 0.61 (0.007) ∗ 0.33 (0.525) 0.49 (0.006) 0.87 (0.062) ∗ 0.54 (0.041) 0.91 (0.011) ∗ 0.88 (0.016) ポール ハーマン 0.59 (0.025) 0.50 (0.001) ∗ 0.74 (0.026) 0.65 (0.001) 0.21 (0.247) 0.55 (0.009) ∗ 0.24 (2.595) 0.63 (0.012) 0.32 (0.447) 0.61 (0.007) ∗ 0.33 (0.525) 0.49 (0.006) 0.87 (0.062) ∗ 0.54 (0.041) 0.91 (0.011) ∗ 0.88 (0.016) 0.56
- CE quality state expansion (new) CEGIS [9] AR [10] Hybrid (new) - CE品質の拡張(新しい) CEGIS [9] AR [10] ハイブリッド(新しい)。 0.82
performance trivial パフォーマンス くだらない 0.61
non-trivial iters time iters time 30 5325 486 非自明なiters time iters time 30 5325 486 0.82
iters time 0.50 0.65 0.38 0.46 0.53 0.42 0.16 0.29 0.50 0.87 Iters 時間 0.50 0.65 0.38 0.46 0.53 0.42 0.16 0.29 0.50 0.87 0.61
(285, 11) 613 6 1801 93 6139 540 (2100, 127) 33 (105, 13) 7 290 5449 49 (146, 17) 301 6069 63 9 2906 2488 299 (631, 143) 23 3172 2782 1215 81 (2374, 545) 76 1 6 9 29 (285, 11) 613 6 1801 93 6139 540 (2100, 127) 33 (105, 13) 7 290 5449 49 (146, 17) 301 6069 63 9 2906 2488 299 (631, 143) 23 3172 2782 1215 81 (2374, 545) 76 1 6 9 29 0.85
12 309 23 615 171 86 643 269 12 309 23 615 171 86 643 269 0.85
17 26 25 (3, 5) 17 26 25 (3, 5) 0.85
(80, 61) (24, 1) (80, 61) (24, 1) 0.85
(485, 13) - (485, 13) - 0.85
- Table 2. CE quality for different methods and performance of three synthesis methods. - 表2。 異なる方法のCE品質と3つの合成法の性能。 0.80
For each model/property, we report results for two different thresholds where the symbol ‘∗’ marks the one closer to the feasibility threshold, representing the more difficult synthesis problem. 各モデル/プロパティについて、より難しい合成問題を表わすため、記号 ‘∗’ が実現可能なしきい値に近い2つの異なるしきい値について結果を報告する。 0.69
Symbol ‘-’ marks a two-hour timeout. シンボル ‘-’ は2時間のタイムアウトを示す。 0.82
CE quality: The presented numbers give the CE quality (i.e., the smaller, the better). CEの品質: 提示された数値はCEの品質を与える(すなわち、より小さいほど良い)。 0.78
The numbers in parentheses represent the average run-time of constructing one CE in seconds (run-times for constructing CE using non-trivial bounds are similar as for trivial ones and are thus not reported). 括弧内の数値は、1つのCEを数秒で構築する平均実行時間を表す(非自明な境界を用いてCEを構築する実行時間は自明なものと似ており、報告されない)。 0.63
Performance: for each method, we report the number of iterations (for the hybrid method, the reported values are iterations of the CEGIS and AR oracle, respectively) and the run-time in seconds. 性能: 各手法について, CEGIS と AR の繰り返し回数と実行時間を数秒で報告する(ハイブリッド手法では, 報告された値はそれぞれ CEGIS と AR の繰り返しである)。 0.82
ratios imply better CEs. 比はcesより優れている。 0.35
To measure the influence of using CEs-modulo-families, two types of bounds are used: (i) trivial bounds (i.e., γ = 0 for safety and γ = 1 for liveness properties), and (ii) non-trivial bounds corresponding to the entire family RD representing the most conservative estimate. CEs-modulo-families を用いることによる影響を測定するために、 (i) 自明な境界(安全のために γ = 0 、生活特性のために γ = 1 )と (ii) 家族 RD に対応する非自明な境界(最も保守的な推定値を表す)の2種類が用いられる。 0.79
The results are reported in (the left part of) Table 2. 結果は表2の(左側)で報告されます。 0.73
In the next subsection, we investigate this same benchmark from the point of view of the performance of the synthesis methods, which also shows the immediate effect of the new CE generation strategy. 次の節では、合成方法のパフォーマンスの観点から、この同じベンチマークを調査します。これは、新しいCE生成戦略の即時の効果も示します。
訳抜け防止モード: 次の節では、合成方法のパフォーマンスの観点から、この同じベンチマークを調査します。 これはまた、新しいCE生成戦略の即時の効果を示しています。
The first observation is that using non-trivial bounds (as opposed to trivial ones) for the state expansion approach can drastically decrease the conflict size. 最初の観測は、状態拡張アプローチに(自明なものとは対照的に)非自明な境界を使用することで、競合サイズを劇的に削減できることである。 0.61
It turns out that the CEs obtained using the greedy approach are mostly larger than those obtained with the MaxSat method. greedyアプローチで得られたcesは、maxsat法で得られたものよりも大体大きいことが判明した。 0.65
However (see Grid ), even for trivial bounds, we may obtain smaller CEs than for MaxSat: computing a minimal-command CE does not necessarily induce an optimal conflict. しかし(グリッド参照)、自明な境界であっても、MaxSat よりも小さな CE を得ることができます。
訳抜け防止モード: しかし(グリッド参照)、自明な境界でも、MaxSatよりも小さなCEを取得できます。 最小限の計算 - コマンドCEは必ずしも最適な競合を引き起こすとは限らない。
On the other hand, comparing the run-times in the parentheses, one can see that computing CEs via the greedy state expansion is orders of magnitude faster than computing command-optimal ones using MaxSat. 一方、括弧内の実行時間を比較すると、greedy状態拡張によるCEの計算は、MaxSatを使ったコマンド最適化の計算よりも桁違いに高速であることがわかる。 0.80
It is good to realize that the greedy method makes at most |K| model-checking queries to compute CEs, while the MaxSat method may make exponentially many such queries. greedyメソッドは最大で |k| モデルチェッククエリを ces の計算に利用し、maxsat メソッドは指数関数的に多くのクエリを作成できる。 0.67
Overall, the greedy method using the non-trivial bounds is able to obtain CEs of comparable quality as the MaxSat method, while being orders of magnitude faster. 全体として、非自明な境界を用いたグリーディ法はmaxsat法と同等の品質のcesが得られるが、桁違いに高速である。 0.62
Inductive Synthesis for Probabilistic Programs Reaches New Horizons 確率的プログラムのための帰納的合成 0.65
15 Performance comparison with AR/CEGIS We compare the hybrid synthesis loop from Sect. 15 AR/CEGISとの性能比較 Sectのハイブリッド合成ループを比較します。 0.84
5 with two state-of-the-art baselines: CEGIS and AR. 最新のベースラインはCEGISとARの2つだ。 0.51
The results are displayed in (the right half of) Table 2. 結果は表2に表示されます(右半分)。 0.74
In all 10 cases, the hybrid method outperforms the baselines. すべての10ケースで、ハイブリッドメソッドはベースラインよりも優れています。 0.60
It is up to an order of magnitude faster. それはマグニチュードのより速い順序まであります。 0.54
Let us discuss the performance of the hybrid method. ハイブリッドメソッドのパフォーマンスについて説明します。 0.69
We classify benchmarks along two dimensions: (1) the performance of CEGIS and (2) the performance of AR. 私たちは、(1)CEGISのパフォーマンスと(2)ARのパフォーマンスの2つの次元に沿ってベンチマークを分類します。
訳抜け防止モード: ベンチマークを2次元に沿って分類する : (1 ) CEGISの性能 および (2 ) AR の性能。
Based on the empirical performance, we classify (Grid ) as good-for-CEGIS (and not for AR), Maze, Pole and DPM as good-for-AR (and not for CEGIS), and Herman as hard (for both). 経験的パフォーマンスに基づいて、(Grid )を(ARではなく)CEGISに、Maze、Pole、DPMを(CEGISではなく)ARに、Hermanを(両方のために)ハードに分類します。 0.69
Roughly, AR works well when the quotient MDP does not blow up and its analysis is precise due to consistent schedulers, i.e., when the parameter dependencies are not crucial for a precise analysis. 概してARは、商 MDP が爆発しておらず、その解析が正確である場合、すなわち、パラメータの依存関係が正確な解析に不可欠でない場合、うまく機能する。 0.72
CEGIS performs well when the CEs are small and fast to compute. CEGISは、CEが小さく、計算が速いときによく機能する。 0.77
On the other hand, synthesis problems for which neither pure CEGIS nor pure AR are able to effectively reason about non-trivial subfamilies, inherently profit from a hybrid method. 一方、純粋なCEGISも純粋なARも、非自明なサブファミリを効果的に推論できない合成問題は、本質的にはハイブリッド手法による利益である。 0.65
The main point we want to discuss is how the hybrid method reinforces the strengths of both methods, rather than their weaknesses. 私たちが議論したい主なポイントは、ハイブリッドメソッドがその弱点ではなく、両方のメソッドの強みをどのように強化するかです。 0.64
In the hybrid method, there are two factors that determine the efficiency: (i) how fast do we get bounds on the reachability probability that are tight enough to enable construction of good counterexamples? ハイブリッド法では, 効率性を決定する因子が2つある: (i) 適切な反例の構築を可能にするのに十分なタイトな到達可能性の限界は, どれくらい高速か? 0.80
and (ii) how good are the constructed counterexamples? そして(ii) 構築された反例はどのくらい良いですか? 0.60
The former factor is attributed to the proposed adaptive scheme (see Alg. 前者の因子は、提案された適応スキームに起因する(Algを参照)。 0.61
2), where the method will prefer AR-like analysis and continue refinement until the computed bounds allow construction of small counterexamples. 2) 計算された境界が小さな反例の構築を可能にするまで,AR 的な解析を優先し,改良を継続する。 0.69
The latter is reflected above. 後者は上記の通りです。 0.69
Let us now discuss how these two aspects are reflected in the benchmarks. この2つの側面がベンチマークでどのように反映されているのかを議論しよう。 0.49
In good-for-CEGIS benchmarks like Grid, after analyzing a quotient MDP for the whole family, the hybrid method mostly profits from better CEs yielding better bounds, thus outperforming CEGIS. GridのようなCEGISベンチマークでは、家族全体の商的MDPを分析した後、このハイブリッド手法はCEがより良いバウンダリを得られることで利益を得ており、CEGISよりも優れています。 0.58
Indeed, the CEs are found so fast that the bottleneck is no longer their generation. 実際、CEはあまりにも速く、ボトルネックはもはや彼らの世代ではない。 0.64
This also explains why the speedup is not immediately translated to the speedup on the overall synthesis loop. これはまた、スピードアップが全体合成ループのスピードアップに即時に変換されない理由を説明する。 0.78
In the good-for-AR benchmark DPM, the hybrid method provides only a minor improvement as it has to perform a large number of AR-iterations before the novel CE-based pruning can be effectively used. The good-for-AR benchmark DPMでは、新しいCEベースのプルーニングを効果的に利用する前に、多数のARイテレーションを実行する必要があるため、ハイブリッド手法は小さな改善しか提供しない。 0.59
This can be considered as the worst-case scenario for the hybrid method. これはハイブリッドメソッドの最悪のシナリオと考えることができる。 0.73
On other good-for-AR benchmarks like Maze and Pole, the good performance on AR allows to quickly obtain tight bounds which can then be exploited by CEGIS. MazeやPoleのような他の優れたARベンチマークでは、ARの優れたパフォーマンスは、CEGISによって悪用されるタイトな境界を迅速に取得することを可能にします。
訳抜け防止モード: MazeやPoleといった他のARベンチマークについて。 ARの優れたパフォーマンスは CEGISで活用可能なタイトなバウンダリを迅速に取得する。
Finally, in hard models like Herman, abstraction-refinement is very expensive, but even the bounds from the first round yield bounds that, as opposed to the trivial bounds, now enable good CEs: CEGIS can keep using these bounds to quickly prune the state space. 最後に、Hermanのようなハードモデルでは、抽象的再定義は非常に高価であるが、第1ラウンドの収差のバウンダリでさえ、自明なバウンダリとは対照的に、良質なCEを実現している: CEGISはこれらのバウンダリを使い続け、状態空間を素早く引き起こすことができる。 0.53
More complicated synthesis problems Our new approach can push the limits of synthesis benchmarks significantly. より複雑な合成問題 我々の新しいアプローチは、合成ベンチマークの限界を著しく押し上げることができる。 0.66
We illustrate this by considering a new variant of the Herman model, Herman∗, and a property imposing an upper bound on the expected number of rounds until stabilization. ハーマンモデルの新しい変種であるハーマン(Herman)と、安定するまで予想されるラウンド数に上限を課す性質を考慮することで、これを説明します。 0.56
We put this bound just below the optimal (i.e., the minimal) value, yielding a hard non-feasible problem. 我々はこの境界を最適値(つまり最小値)のすぐ下に置くと、難しい非実現不可能な問題をもたらす。 0.72
The synthesis results are summarized in Table 3. 合成結果は表3にまとめられている。 0.88
As CEGIS performs poorly on Herman, it is excluded here. CEGISはヘルマンでうまく動作しないため、ここでは除外されます。 0.56
16 R. Andriushchenko et al. 16 r. andriushchenkoら。 0.77
AR Hybrid iters AR ハイブリッド Iters 0.75
synthesis synthesis iters time problem iters time problem feasibility 81 69k 47h (14280, 2) 13.4m feasibility two properties 97 optimality 83k 55h (16197, 3) 16.8m optimality 5%-optimality 60k 42h (6421, 7) 5.1m Table 3. 合成合成 iters time problem iters time problem iters time problem 47h (14280, 2) 13.4m feasibility two properties 97 optimality 83k 55h (16197, 3) 16.8m optimality 5%-optimality 60k 42h (6421, 7) 5.1m table 3 0.87
The impact of scaling the family size (of the Herman∗ model) and handling more complex synthesis problems. ファミリーサイズ(ヘルマン∗モデルの)のスケールとより複雑な合成問題への対処の影響。 0.79
The left part shows the results for the smaller variant (5k members), the right part for the larger one (3.1M members). 左の部分は、より小さい変種(5kメンバー)、大きいもの(3.1Mメンバー)の結果を示している。 0.77
time 30s (274, 1) 7s 38s (274, 1) 8s 531 150s (571, 7) 12s time 30s (274, 1) 7s 38s (274, 1) 8s 531 150s (571, 7) 12s 0.94
Hybrid iters ハイブリッド Iters 0.70
time AR First, we investigate on small Herman∗ how the methods can handle the synthesis for multi-property specifications. 時間 AR まず,このメソッドがマルチプロパティ仕様の合成をどのように処理できるかについて検討する。 0.72
We add one feasible property to the (still non-feasible) specification (row ‘two properties’). 実行可能なプロパティを(まだ実現不可能な)仕様に1つ追加します(row ‘two properties’)。 0.65
While including more properties typically slows down the AR computation, the performance of the hybrid method is not affected as the corresponding overhead is mitigated by additional pruning opportunities. より多くのプロパティを含むことでar計算が遅くなるが、対応するオーバーヘッドが追加のプルーニングの機会によって軽減されるため、ハイブリッドメソッドのパフォーマンスは影響を受けない。 0.58
Second, we consider optimal synthesis for the property as used in the feasibility synthesis. 第二に、実現性合成における特性の最適合成を検討する。 0.80
The hybrid method requires only a minor overhead to find an optimal solution compared to checking feasibility. ハイブリッド手法は, 検査可能性よりも最適な解を見つけるために, ほんの少しのオーバーヘッドしか必要としない。
訳抜け防止モード: ハイブリッド方式はわずかなオーバーヘッドしか必要としない 検査可能性よりも最適な解を求める。
This overhead is significantly larger for AR. このオーバーヘッドはARにとってかなり大きい。 0.69
Next, we consider larger Herman∗ model having significantly more randomization strategies (3.1M members) that include solutions leading to a considerably faster stabilization. 次に、より大きなヘルマンシュモデルは、かなり速い安定化につながるソリューションを含む、かなり多くのランダム化戦略(3.1Mメンバー)を有すると考えます。
訳抜け防止モード: 次に、より大きな確率化戦略を持つHerman∗モデルを考える。 (3.1M) より高速な安定化につながる解決策が 含まれています
This model is out of reach for existing synthesis approaches: one-by-one enumeration takes more than 27 hours and the AR performs even worse—solving the feasibility and optimality problems requires 47 and 55 hours, respectively. 一つずつの列挙に27時間以上を要し、arの性能はさらに悪化し、実現可能性と最適性の問題にそれぞれ47時間と55時間を要する。
訳抜け防止モード: このモデルは既存の合成アプローチには及ばない 1----- 列挙には27時間以上かかる ARの動作はさらに悪くなります 実現可能性と最適性の問題 それぞれ47時間55時間です
On the other hand, the proposed hybrid method is able to solve these problems within minutes. 一方,提案されたハイブリッド手法は,これらの問題を数分で解くことができる。 0.78
Finally, we consider a relaxed variant of optimal synthesis (5%-optimality) guaranteeing that the found solution is up to 5% worse than the optimal. 最後に、最適な合成(5%最適)の緩和された変種を検討し、その解が最適よりも最大5%悪いことを保証した。 0.74
Relaxing the optimally criterion speeds up the hybrid synthesis method by about a factor three. 最適な基準を緩和すると、ハイブリッド合成方法が約3倍速くなります。 0.70
These experiments clearly demonstrate that scaling up the synthesis problem several orders of magnitude renders existing synthesis methods infeasible: they need tens of hours to solve the synthesis problems. これらの実験は、合成問題を数桁のスケールアップすると、既存の合成方法が実現不可能となることを明らかに示している。 0.67
Meanwhile, the hybrid method tackles these difficult synthesis problems without significant penalty and is capable of producing a solution within minutes. 一方,ハイブリッド法は,このような難解な合成問題に対して大きなペナルティを課さずに対処し,数分で解を生成できる。
訳抜け防止モード: 一方 ハイブリッド法は 重大なペナルティを伴わずに この難解な合成問題に取り組む 数分で解を作ることができます
7 Conclusion We present a novel method for the automated synthesis of probabilistic programs. 7 結論 本稿では,確率的プログラムの自動合成手法を提案する。 0.73
Pairing the counterexample-guide d inductive synthesis with the deductive oracle using an MDP abstraction, we develop a synthesis technique enabling faster construction of smaller counterexamples. MDPを抽象化した導出オラクルを用いた反例誘導誘導型インダクティブ合成により,より小さな反例を高速に構築できる合成技術を開発した。 0.69
Evaluating the method on case studies from different domains, we demonstrate that the novel CE construction and the adaptive strategy lead to a significant acceleration of the synthesis process. 異なる領域のケーススタディにおける手法の評価を行い,新しいce構築法と適応戦略が合成過程の大幅な加速に寄与することを示した。 0.78
The proposed method is able to reduce the run-time for challenging problems from days to minutes. 提案手法は,問題発生時の実行時間を数日から数分に短縮できる。 0.73
In our future work, we plan to investigate counterexamples on the quotient MDPs and improve the abstraction refinement strategy. 今後の作業では、商MDPの反例を調査し、抽象化の改良戦略を改善する予定です。 0.62
Inductive Synthesis for Probabilistic Programs Reaches New Horizons 確率的プログラムのための帰納的合成 0.65
17 References 1. 17 参考文献 1. 0.79
´Abrah´am, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J.P., Wimmer, R.: Counterexample generation for discrete-time Markov models: An introductory survey. Abrah ́am, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J.P., Wimmer, R.: 離散時間マルコフモデルに対する反例生成: 導入調査。 0.84
In: SFM. LNCS, vol. 略称はSFM。 LNCS, vol。 0.67
8483, pp. 65–121. 8483, pp。 65–121. 0.76
Springer (2014) Springer (複数形 Springers) 0.60
2. Alur, R., Bod´ık, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. 2. Alur, R., Bod ́k, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. 0.91
In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, vol. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, vol。 0.79
40, pp. 1–25. 40, pp。 1–25. 0.76
IOS Press (2015) IOS Press (2015) 0.85
3. Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic 3. Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic 0.87
systems. In: Handbook of Model Checking, pp. システム。 In: Handbook of Model Checking, pp。 0.75
963–999. Springer (2018) 963–999. Springer (複数形 Springers) 0.64
4. Baier, C., Hensel, C., Hutschenreiter, L., Junges, S., Katoen, J., Klein, J.: Parametric markov chains: PCTL complexity and fraction-free gaussian elimination. 4. Baier, C., Hensel, C., Hutschenreiter, L., Junges, S., Katoen, J., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination。 0.87
Inf. Comput. インフ。 Comput 0.43
272, 104504 (2020) 272, 104504 (2020) 0.85
5. Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. 5. Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: 確率システムのモデル修復。 0.89
In: TACAS’11. で:TACAS'11。 0.63
LNCS, vol. LNCS, vol。 0.79
6605, pp. 326–340 (2011) 6. 6605, pp。 326–340 (2011) 6. 0.86
Bornholt, J., Torlak, E., Grossman, D., Ceze, L.: Optimizing synthesis with metas- Bornholt, J., Torlak, E., Grossman, D., Ceze, L.: Metasによる合成の最適化- 0.88
ketches. In: POPL’16. ケッチ In:POPL’16。 0.50
p. 775–788. Association for Computing Machinery (2016) 775-788頁。 Association for Computing Machinery (2016) 0.74
7. Calinescu, R., ˇCeˇska, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Efficient synthesis of robust models for stochastic systems. 7. Calinescu, R., シュケシュカ, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: 確率系に対する頑健なモデルの効率的な合成。 0.85
J. of Systems and Softw. J. of Systems and Softw 0.78
143, 140–158 (2018) 143, 140–158 (2018) 0.92
8. ˇCeˇska, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: Precise parameter synthesis for stochastic biochemical systems. 8. M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: 確率的生化学系の精密パラメータ合成
訳抜け防止モード: 8. シュケシュカ, M., Dannenberg, F., Paoletti, N. Kwiatkowska, M., Brim, L. : 確率的生化学系のための精密パラメータ合成
Acta Inf. acta inf所属。 0.60
54(6), 589–623 (2017) 54(6), 589–623 (2017) 0.94
9. ˇCeˇska, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-drive n synthesis for probabilistic program sketches. 9. シュチェスカ, m., hensel, c., junges, s., katoen, j.p.: counterexample-drive n synthesis for probabilistic program sketches. 0.87
In: FM. LNCS, vol. 略称:fm。 LNCS, vol。 0.66
11800, pp. 101–120. 11800年、p。 101–120. 0.72
Springer (2019) Springer (複数形 Springers) 0.62
10. ˇCeˇska, M., Jansen, N., Junges, S., Katoen, J.P.: Shepherding hordes of Markov 10. シュチェシュカ, M., Jansen, N., Junges, S., Katoen, J.P.: マルコフの羊飼い 0.79
chains. In: TACAS (2). 鎖だ 内:TACAS (2)。 0.66
LNCS, vol. LNCS, vol。 0.79
11428, pp. 172–190. 11428、p。 172–190. 0.71
Springer (2019) Springer (複数形 Springers) 0.62
11. Chatzieleftheriou, G., Katsaros, P.: Abstract model repair for probabilistic systems. 11. Chatzieleftheriou, G., Katsaros, P.:確率システムの抽象モデル修復。 0.82
Inf. Comput. インフ。 Comput 0.43
259(1), 142–160 (2018) 259(1), 142–160 (2018) 0.94
12. Chonev, V.: Reachability in augmented interval Markov chains. 12. Chonev, V.: 拡張間隔マルコフ鎖の到達性。 0.79
In: RP’2019. で:RP'2019。 0.72
LNCS, vol. 11674, pp. LNCS Vol. 11674, pp。 0.65
79–92. Springer (2019) 79–92. Springer (複数形 Springers) 0.66
13. Chrszon, P., Dubslaff, C., Kl¨uppelholz, S., Baier, C.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. 13. Chrszon, P., Dubslaff, C., Kl suppelholz, S., Baier, C.: ProFeat: 家族ベースの確率モデルチェックのための機能指向エンジニアリング。 0.86
Formal Asp. Comput. 正式な asp. Comput 0.55
30(1), 45–75 (2018) 30(1), 45–75 (2018) 0.94
14. Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y. 14. Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y。 0.89
: Model checking software product lines with SNIP. SNIPを用いたソフトウェア製品ラインのモデル検査 0.78
Int. J. on Softw. Int J. on Softw 0.63
Tools for Technol. Technolのツール。 0.72
Transf. 14, 589–612 (2012) トランスf。 14, 589–612 (2012) 0.78
15. Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. 15. Daws, C.: 離散時間マルコフ連鎖のシンボリックおよびパラメトリックモデル検査。 0.80
In: ICTAC. LNCS, vol. In:ICTAC。 LNCS, vol。 0.76
3407, pp. 280–294. 3407, pp。 280–294. 0.76
Springer (2004) Springer (複数形 Springers) 0.58
16. Dehnert, C., Jansen, N., Wimmer, R., ´Abrah´am, E., Katoen, J.P.: Fast debugging 16. Dehnert, C., Jansen, N., Wimmer, R., ́Abrah ́am, E., Katoen, J.P.: 高速デバッグ 0.85
of PRISM models. In: ATVA. PRISMモデル。 ATVA所属。 0.48
LNCS, vol. LNCS, vol。 0.79
8837, pp. 146–162. 8837, pp。 146–162. 0.75
Springer (2014) Springer (複数形 Springers) 0.60
17. Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.P., ´Abrah´am, E.: PROPhESY: A PRObabilistic ParamEter SYNnthesis Tool. 17. Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.P., ́Abrah ́am, E.: PROPhESY: A PRObabilistic ParamEter Synnthesis Tool。 0.90
In: CAV’15. LNCS, vol. で:CAV'15。 LNCS, vol。 0.77
9206, pp. 214–231. 9206, pp。 214–231. 0.75
Springer (2015) Springer (複数形 Springers) 0.60
18. Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A Storm is coming: A modern probabilistic model checker. 18. Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A Storm is coming: a modern probabilistic model checker。 0.89
In: CAV. LNCS, vol. 略称:CAV。 LNCS, vol。 0.71
10427, pp. 10427, pp。 0.80
592–600. Springer (2017) 592–600. Springer (複数形 Springers) 0.63
18 R. Andriushchenko et al. 18 r. andriushchenkoら。 0.77
19. Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for probabilistic reachability constraints. 19. funke, f., jantsch, s., baier, c.: farkas certificates and minimal witnesss for probabilistic reachability constraints (英語) 0.83
In: TACAS (1). 内:TACAS (1)。 0.71
LNCS, vol. LNCS, vol。 0.79
12078, pp. 324–345. 12078年、p。 324–345. 0.73
Springer (2020) Springer (複数形 Springers) 0.62
20. Gerasimou, S., Calinescu, R., Tamburrelli, G.: Synthesis of probabilistic models for quality-of-service software engineering. 20. Gerasimou, S., Calinescu, R., Tamburrelli, G.: サービス品質のソフトウェアエンジニアリングのための確率モデルの合成。 0.87
Autom. Softw. Eng. 自動。 柔らかくて Eng! 0.63
25(4), 785–831 (2018) 21. 25(4), 785–831 (2018) 21. 0.92
Ghezzi, C., Sharifloo, A.M.: Model-based verification of quantitative non-functional properties for software product lines. Ghezzi, C., Sharifloo, A.M.: ソフトウェア製品ラインの定量的非機能特性のモデルによる検証。 0.78
Inf. & Softw. インフ。 とSoftw。 0.52
Technol. 55(3), 508–524 (2013) 22. テクノ。 55(3), 508–524 (2013) 22. 0.80
Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Hahn, E.M., Hermanns, H., Zhang, L.:パラメトリックの確率的到達性 0.82
Markov models. Int. マルコフモデル。 Int 0.54
J. on Softw. J. on Softw 0.77
Tools for Technol. Technolのツール。 0.72
Transf. 13(1), 3–19 (2011) トランスf。 13(1), 3–19 (2011) 0.79
23. Harman, M., Mansouri, S.A., Zhang, Y.: Search-based software engineering: Trends, 23. Harman, M., Mansouri, S.A., Zhang, Y.: Search-based software engineering: Trends, 0.89
techniques and applications. ACM Comp. 技術および適用。 ACMの略。 0.66
Surveys 45(1), 11:1–11:61 (2012) 45(1), 11:1–11:61 (2012) 0.78
24. Herman, T.: Probabilistic self-stabilization. 24. Herman, T.:確率的自己安定化。 0.77
Inf. Process. インフ。 プロセス。 0.58
Lett. 35(2), 63–67 (1990) 25. Lett! 35(2), 63–67 (1990) 25. 0.78
Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle ガイドコンポーネントベース 0.87
program synthesis. In: ICSE. プログラム合成。 内: ICSE。 0.74
p. 215–224. p.215-224。 0.59
ACM (2010) ACM (2010) 0.85
26. Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic verification of Herman’s self-stabilisation algorithm. 26. Kwiatkowska, M., Norman, G., Parker, D.: Hermanの自己安定化アルゴリズムの確率的検証。 0.87
Formal Aspects of Computing 24(4), 661–670 (2012) 27. 計算の形式的側面 24(4), 661–670 (2012) 27。 0.72
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic 0.98
real-time systems. リアルタイムシステム。 0.78
In: CAV. LNCS, vol. 略称:CAV。 LNCS, vol。 0.71
6806, pp. 585–591. 6806, pp。 585–591. 0.75
Springer (2011) Springer (複数形 Springers) 0.62
28. Lanna, A., Castro, T., Alves, V., Rodrigues, G., Schobbens, P.Y., Apel, S.: Featurefamily-based reliability analysis of software product lines. 28. Lanna, A., Castro, T., Alves, V., Rodrigues, G., Schobbens, P.Y., Apel, S.: ソフトウェア製品ラインの機能ファミリベースの信頼性分析。 0.86
Inf. and Softw. インフ。 そして、Softw。 0.50
Technol. 94, 59–81 (2018) テクノ。 94, 59–81 (2018) 0.80
29. Lindemann, C.: Performance modelling with deterministic and stochastic Petri nets. 29. Lindemann, C.: 決定論的および確率論的ペトリネットによるパフォーマンスモデリング。 0.78
Eval. Rev. 26(2), 3 (1998) Eval Rev 26(2), 3 (1998) 0.59
30. Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and infinite-horizon partially observable Markov decision problems. 30. マダニ, O., Hanks, S., Condon, A.:確率計画と無限水平部分観測可能なマルコフ決定問題の不決定性について 0.83
pp. 541–548. pp. 541–548. 0.78
AAAI Press / The MIT Press (1999) AAAI Press / The MIT Press (1999年) 0.85
31. Martens, A., Koziolek, H., Becker, S., Reussner, R.: Automatically improve software architecture models for performance, reliability, and cost using evolutionary algorithms. 31. Martens, A., Koziolek, H., Becker, S., Reussner, R.: 進化的アルゴリズムを使ってソフトウェアアーキテクチャモデルのパフォーマンス、信頼性、コストを自動的に改善する。 0.85
pp. 105–116. pp. 105–116. 0.78
ACM (2010) ACM (2010) 0.85
32. Nori, A.V., Ozair, S., Rajamani, S.K., Vijaykeerthy, D.: Efficient synthesis of 32. Nori, A.V., Ozair, S., Rajamani, S.K., Vijaykeerthy, D.: 効率的な合成 0.86
probabilistic programs. In: PLDI’14. 確率的プログラム。 In:PLDI'14。 0.75
pp. 208–217. pp. 208–217. 0.78
ACM (2015) ACM (2015) 0.85
33. Oliehoek, F.A., Amato, C.: A Concise Introduction to Decentralized POMDPs. 33. Oliehoek, F.A., Amato, C.: A Concise Introduction to Decentralized POMDPs 0.89
Springer Briefs in Intelligent Systems, Springer (2016) Springer、Intelligent Systems、Springerの略(2016年) 0.76
34. Pathak, S., ´Abrah´am, E., Jansen, N., Tacchella, A., Katoen, J.P.: A greedy approach for the efficient repair of stochastic models. 34. Pathak, S., ́Abrah ́am, E., Jansen, N., Tacchella, A., Katoen, J.P.: 確率モデルの効率的な修復のための欲深いアプローチ。 0.84
In: NFM’15. LNCS, vol. で:NFM'15。 LNCS, vol。 0.71
9058, pp. 295– 309. 9058年、p。 295– 309. 0.83
Springer (2015) Springer (複数形 Springers) 0.60
35. Puterman, M.L. 35. パターマン、M.L。 0.66
: Markov Decision Processes: Discrete Stochastic Dynamic Pro- : Markov Decision Processes: Discrete Stochastic Dynamic Pro- 0.94
gramming. Wiley Series in Probability and Statistics, Wiley (1994) グラミング Wiley Series in Probability and Statistics, Wiley (1994) 0.60
36. Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.P.: Parameter synthesis for Markov models: Faster than ever. 36. Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.P.: Markovモデルのパラメータ合成: これまで以上に速い。 0.90
In: ATVA’16. 内:ATVA'16。 0.70
LNCS, vol. LNCS, vol。 0.79
9938, pp. 50–67 (2016) 9938, pp。 50–67 (2016) 0.82
37. Quatmann, T., Jansen, N., Dehnert, C., Wimmer, R., ´Abrah´am, E., Katoen, J.P., Becker, B.: Counterexamples for expected rewards. 37. Quatmann, T., Jansen, N., Dehnert, C., Wimmer, R., ́Abrah ́am, E., Katoen, J.P., Becker, B.: Counterexamples for expected rewards。 0.92
In: FM. pp. 略称:fm。 pp. 0.69
435–452. Springer (2015) 435–452. Springer (複数形 Springers) 0.65
38. Saad, F.A., Cusumano-Towner, M.F., Schaechtle, U., Rinard, M.C., Mansinghka, V.K. 38. Saad, F.A., Cusumano-Towner, M.F., Schaechtle, U., Rinard, M.C., Mansinghka, V.K. 0.82
: Bayesian synthesis of probabilistic programs for automatic data modeling. : 自動データモデリングのための確率的プログラムのベイズ的合成 0.84
Proceedings of the ACM on Programming Languages 3(POPL), 1–32 (2019) プログラミング言語3(POPL),1-32(2019)におけるACMの進捗状況 0.88
39. Solar-Lezama, A., Rabbah, R., Bod´ık, R., Ebcio˘glu, K.: Programming by sketching 39. Solar-Lezama, A., Rabbah, R., Bod ́ık, R., Ebcio sglu, K.: スケッチによるプログラミング 0.84
for bit-streaming programs. ビットストリーミングプログラム用。 0.80
In: PLDI’05. で:PLDI'05。 0.68
pp. 281–294. pp. 281–294. 0.78
ACM (2005) ACM (2005) 0.85
Inductive Synthesis for Probabilistic Programs Reaches New Horizons 確率的プログラムのための帰納的合成 0.65
19 40. Vandin, A., ter Beek, M.H., Legay, A., Lluch-Lafuente, A.: Qflan: A tool for the quantitative analysis of highly reconfigurable systems. 19 40. Vandin, A., ter Beek, M.H., Legay, A., Lluch-Lafuente, A.: Qflan: 高度に再構成可能なシステムの定量的解析ツール。 0.86
In: FM. LNCS, vol. 略称:fm。 LNCS, vol。 0.66
10951, pp. 10951, pp。 0.80
329–337. Springer (2018) 329–337. Springer (複数形 Springers) 0.64
41. Wimmer, R., Jansen, N., Vorpahl, A., ´Abrah´am, E., Katoen, J.P., Becker, B.: Highlevel counterexamples for probabilistic automata. 41. Wimmer, R., Jansen, N., Vorpahl, A., ́Abrah ́am, E., Katoen, J.P., Becker, B.: 確率的オートマトンに対する高レベルの反例。 0.82
Logical Methods in Computer Science 11(1) (2015) コンピュータサイエンスにおけるロジカル手法11(1)(2015年) 0.76
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecomm ons.org/licenses/by/ 4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. Open Access この章はCreative Commons Attribution 4.0 International License (http://creativecomm ons.org/licenses/by/ 4.0/)の条項でライセンスされており、オリジナルの作者とソースに適切なクレジットを与え、Creative Commonsライセンスへのリンクを提供し、変更が行われたかどうかを示す。 0.73
The images or other third party material in this chapter are included in the chapter’s Creative Commons license, unless indicated otherwise in a credit line to the material. この章の画像やその他の第三者の資料は、資料へのクレジットラインに別段の記載がない限り、章のクリエイティブコモンズライセンスに含まれています。 0.72
If material is not included in the chapter’s Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. 素材が章のクリエイティブコモンズライセンスに含まれておらず、あなたの意図された使用が法定規制によって許可されていないか、許可された使用を超える場合は、著作権者から直接許可を得る必要があります。
訳抜け防止モード: 資料が第 章のクリエイティブ・コモンズ・ライセンスに含まれていない場合 法定規制により許可されないか、又は許可された使用を超過する。 著作権者から直接許可を得る必要があります。

翻訳にはFugu-Machine Translatorを利用しています。