检索结果-内蒙古大学图书馆

43rd International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE)

作者： Goel, Aman Merz, Stephan Sakallah, Karem A. Amazon Web Serv Seattle WA 98019 USA Univ Lorraine LORIA Inria CNRS Nancy France Univ Michigan Ann Arbor MI 48109 USA

ISBN: (纸本)9783031353543;9783031353550

The Bakery algorithm is a landmark algorithm for ensuring mutual exclusion among N processes that communicate via shared variables. Starting from existing TLA(+) specifications, we use the recentlydeveloped IC3PO parameterized model checker to automatically compute inductive invariants for two versions of the algorithm. We compare the machine-generated invariants with human-written invariants that were used in an interactive correctness proof checked by the TLA(+) Proof System. Our experience suggests that automated invariant inference is becoming a viable alternative to labor-intensive human-written proofs.

关键词： parameterized verification mutual exclusion inductive invariant

来源：评论

学校读者我要写书评

暂无评论

The complexity of verifying population protocols

引用

DISTRIBUTED COMPUTING 2021年第2期34卷 133-177页

作者： Esparza, Javier Jaax, Stefan Raskin, Mikhail Weil-Kennedy, Chana Tech Univ Munich Munich Germany

Population protocols (Angluin et al. in PODC, 2004) are a model of distributed computation in which indistinguishable, finitestate agents interact in pairs to decide if their initial configuration, i.e., the initial number of agents in each state, satisfies a given property. In a seminal paper Angluin et al. classified population protocols according to their communication mechanism, and conducted an exhaustive study of the expressive power of each class, that is, of the properties they can decide (Angluin et al. in Distrib Comput 20(4):279-304, 2007). In this paper we study the correctness problem for population protocols, i.e., whether a given protocol decides a given property. A previous paper (Esparza et al. in Acta Inform 54(2):191-215, 2017) has shown that the problem is decidable for the main population protocol model, but at least as hard as the reachability problem for Petri nets, which has recently been proved to have non-elementary complexity. Motivated by this result, we study the computational complexity of the correctness problem for all other classes introduced by Angluin et al., some of which are less powerful than the main model. Our main results show that for the class of observation models the complexity of the problem is much lower, ranging from Pi(p)(2) to PSPACE.

关键词： Reachability analysis parameterized verification Population protocols Distributed computing

来源：评论

学校读者我要写书评

暂无评论

CONTROLLING A RANDOM POPULATION

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2021年第4期17卷 12:1-12:21页

作者： Colcombet, Thomas Fijalkow, Nathanael Ohlmann, Pierre Univ Paris CNRS Paris France Univ Bordeaux LaBRI CNRS Bordeaux France Alan Turing Inst Data Sci London England Univ Paris Paris France

Bertrand et al. introduced a model of parameterised systems, where each agent is represented by a finite state system, and studied the following control problem: for any number of agents, does there exist a controller able to bring all agents to a target state? They showed that the problem is decidable and EXPTIME-complete in the adversarial setting, and posed as an open problem the stochastic setting, where the agent is represented by a Markov decision process. In this paper, we show that the stochastic control problem is decidable. Our solution makes significant uses of well quasi orders, of the max-flow min-cut theorem, and of the theory of regular cost functions. We introduce an intermediate problem of independence interest called the sequential flow problem and study its complexity.

关键词： parameterized verification Population Protocols parameterized Synthesis Markov Decision Processes Regular Cost Functions Games

来源：评论

学校读者我要写书评

暂无评论

A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries 1

引用

22nd International Conference on verification, Model Checking, and Abstract Interpretation (VMCAI) jointly with the 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)

作者： Bertrand, Nathalie Lazic, Marijana Widder, Josef Univ Rennes CNRS INRIA IRISA Rennes France Tech Univ Munich Munich Germany Informal Syst Vienna Austria

ISBN: (数字)9783030670672

ISBN: (纸本)9783030670665;9783030670672

Weak adversaries are a way to model the uncertainty due to asynchrony in randomized distributed algorithms. They are a standard notion in correctness proofs for distributed algorithms, and express the property that the adversary (scheduler), which has to decide which messages to deliver to which process, has no means of inferring the outcome of random choices, and the content of the messages. In this paper, we introduce a model for randomized distributed algorithms that allows us to formalize the notion of weak adversaries. It applies to randomized distributed algorithms that proceed in rounds and are tolerant to process failures. For this wide class of algorithms, we prove that for verification purposes, the class of weak adversaries can be restricted to simple ones, so-called round-rigid adversaries, that keep the processes tightly synchronized. As recently a verification method for round-rigid adversaries has been introduced, our new reduction theorem paves the way to the parameterized verification of randomized distributed algorithms under the more realistic weak adversaries.

关键词： Communication closure Reduction Distributed algorithms Randomized consensus Weak adversaries parameterized verification

来源：评论

学校读者我要写书评

暂无评论

Fine-Grained Complexity of Safety verification

引用

JOURNAL OF AUTOMATED REASONING 2020年第7期64卷 1419-1444页

作者： Chini, Peter Meyer, Roland Saivasan, Prakash TU Braunschweig Braunschweig Germany

We study the fine-grained complexity of Leader Contributor Reachability (LCR) and Bounded-Stage Reachability (BSR), two variants of the safety verification problem for shared memory concurrent programs. For both problems, the memory is a single variable over a finite data domain. Our contributions are new verification algorithms and lower bounds. The latter are based on the Exponential Time Hypothesis (ETH), the problem Set Cover, and cross-compositions. LCR is the question whether a designated leader thread can reach an unsafe state when interacting with a certain number of equal contributor threads. We suggest two parameterizations: (1) By the size of the data domain D and the size of the leader L, and (2) by the size of the contributors C. We present algorithms for both cases. The key techniques are compact witnesses and dynamic programming. The algorithms run in O* ((L . (D + 1))(L.D) . D-D ) and O* (2(C)) time, showing that both parameterizations are fixed-parameter tractable. We complement the upper bounds by (matching) lower bounds based on ETH and Set Cover. Moreover, we prove the absence of polynomial kernels. For BSR, we consider programs involving t different threads. We restrict the analysis to computations where the write permission changes s times between the threads. BSR asks whether a given configuration is reachable via such an s-stage computation. When parameterized by P, the maximum size of a thread, and t, the interesting observation is that the problem has a large number of difficult instances. Formally, we show that there is no polynomial kernel, no compression algorithm that reduces the size of the data domain D or the number of stages s to a polynomial dependence on P and t. This indicates that symbolic methods may be harder to find for this problem.

关键词： parameterized verification parameterized complexity Fine-grained complexity Safety verification

来源：评论

学校读者我要写书评

暂无评论

Accelerated verification of Parametric Protocols with Decision Trees 38

Accelerated Verification of Parametric Protocols with Decisi...

引用

38th IEEE International Conference on Computer Design (ICCD)

作者： Li, Yongjian Cao, Taifeng Jansen, David N. Pang, Jun Wei, Xiaotao Chinese Acad Sci Inst Software State Key Lab Comp Sci Beijing Peoples R China Beijing Jiaotong Univ Sch Software Engn Beijing Peoples R China Reliabil & Trust Univ Luxembourg Technol & Med Interdisciplinary Ctr Secur Fac Sci Esch Sur Alzette Luxembourg

ISBN: (纸本)9781728197104

Within a framework for verifying parametric network protocols through induction, one needs to find invariants based on a protocol instance of a small number of nodes. In this paper, we propose a new approach to accelerate parameterized verification by adopting decision trees to represent the state space of a protocol instance. Such trees can be considered as a knowledge base that summarizes all behaviors of the protocol instance. With this knowledge base, we are able to efficiently construct an oracle to effectively assess candidates of invariants of the protocol, which are suggested by an invariant finder. With the discovered invariants, a formal proof for the correctness of the protocol can be derived in the framework after proper generalization. The effectiveness of our method is demonstrated by experiments with typical benchmarks.

关键词： Formal methods parameterized verification machine learning decision trees cache coherence protocols

来源：评论

学校读者我要写书评

暂无评论

Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs 1

引用

18th International Symposium on Automated Technology for verification and Analysis (ATVA)

作者： Esparza, Javier Helfrich, Martin Jaax, Stefan Meyer, Philipp J. Tech Univ Munich Munich Germany

ISBN: (数字)9783030591526

ISBN: (纸本)9783030591526;9783030591519

We present a new version of Peregrine, the tool for the analysis and parameterized verification of population protocols introduced in [Blondin et al., CAV'2018]. Population protocols are a model of computation, intensely studied by the distributed computing community, in which mobile anonymous agents interact stochastically to perform a task. Peregrine 2.0 features a novel verification engine based on the construction of stage graphs. Stage graphs are proof certificates, introduced in [Blondin et al., CAV'2020], that are typically succinct and can be independently checked. Moreover, unlike the techniques of Peregrine 1.0, the stage graph methodology can verify protocols whose executions never terminate, a class including recent fast majority protocols. Peregrine 2.0 also features a novel proof visualization component that allows the user to interactively explore the stage graph generated for a given protocol.

关键词： Population protocols Distributed computing parameterized verification Stage graphs

来源：评论

学校读者我要写书评

暂无评论

Complexity of verification and Synthesis of Threshold Automata 1

引用

18th International Symposium on Automated Technology for verification and Analysis (ATVA)

作者： Balasubramanian, A. R. Esparza, Javier Lazic, Marijana Tech Univ Munich Munich Germany

ISBN: (数字)9783030591526

ISBN: (纸本)9783030591526;9783030591519

Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed by a fixed but arbitrary number of processes. We conduct the first systematic study of the complexity of verification and synthesis problems for threshold automata. We prove that the coverability, reachability, safety, and liveness problems are NP-complete, and that the bounded synthesis problem is Sigma(2)(p) complete. A key to our results is a novel characterization of the reachability relation of a threshold automaton as an existential Presburger formula. The characterization also leads to novel verification and synthesis algorithms. We report on an implementation, and provide experimental results.

关键词： Threshold automata Distributed algorithms parameterized verification

来源：评论

学校读者我要写书评

暂无评论

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling 32nd

Checking Qualitative Liveness Properties of Replicated Syste...

引用

32nd International Conference on Computer-Aided verification (CAV)

作者： Blondin, Michael Esparza, Javier Helfrich, Martin Kucera, Antonin Meyer, Philipp J. Univ Sherbrooke Sherbrooke PQ Canada Tech Univ Munich Munich Germany Masaryk Univ Brno Czech Republic

ISBN: (纸本)9783030532918;9783030532901

We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.

关键词： parameterized verification Liveness Stochastic systems

来源：评论

学校读者我要写书评

暂无评论

verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking 1

引用

International Conference on verification, Model Checking, and Abstract Interpretation (VMCAI)

作者： Andre, Etienne Fribourg, Laurent Mota, Jean-Marc Soulat, Romain Univ Paris 13 LIPN CNRS UMR 7030 F-93430 Villetaneuse France CNRS JFLI Tokyo Japan Natl Inst Informat Tokyo Japan Univ Paris Saclay LSV ENS Paris Saclay Paris France Univ Paris Saclay CNRS Paris France Univ Paris Saclay INRIA Paris France Thales Res & Technol Palaiseau France

ISBN: (数字)9783030112455

ISBN: (纸本)9783030112455;9783030112448

The election of a leader in a network is a challenging task, especially when the processes are asynchronous, i. e., execute an algorithm with time-varying periods. Thales developed an industrial election algorithm with an arbitrary number of processes, that can possibly fail. In this work, we prove the correctness of a variant of this industrial algorithm. We use a method combining abstraction, the SafeProver solver, and a parametric timed model-checker. This allows us to prove the correctness of the algorithm for a large number p of processes (p = 5000).

关键词： Leader election Distributed algorithm Model checking SaveProver parameterized verification Parametric timed automata

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：