SI2 - SSE: A Next-Generation Decision Diagram Library

SI2 - SSE：下一代决策图库

• 批准号: 1642397
• 负责人: Andrew Miner
• 金额: $ 49.87万
• 依托单位: Iowa State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-01-01 至 2021-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1642397&HistoricalAwards=false
• 关键词: SI2; SSE; Next; Generation; Decision

There are a variety of scientific problems whose solution is made difficult because of the extremely large number of possibilities that must be considered and evaluated. Often, the difficulty is caused by a large number of combinations of interacting components, even though the individual components are relatively simple. Relevant practical problems are measuring the reliability of a communication network where links may fail (made difficult by the number of different communication paths in the network), or determining that an automobile's brakes will always work (made difficult by the number of combinations of the interacting software and hardware components in an automobile), or determining that the failure of one power generator will not cause a cascading failure that affects a large portion of the nation's power grid. This class of problem is conceptually similar to finding an optimal solution for Rubik's cube (which is made difficult by the large number of different possible configurations) or, in chess, determining if there is a sequence of moves in chess such that white can always force a win (made difficult by the huge number of different possible chess games). The goal of this project is to develop a software library called Meddly that various applications can use to build and represent solutions to these types of combinatoric problems. The underlying technology of Meddly is decision diagrams, a mechanism for organizing data in such a way that repeated patterns or subpatterns are automatically discovered and exploited during computation. The project will add to the capabilities of decision diagram technology, help to advance the understanding of this technology as well as apply it to more types of problems. Several researchers from around the world have expressed interest in Meddly, and as part of this project, developers will assist those researchers to integrate Meddly into existing tools, which will then be applied to real problems. The project also has educational goals, through the engagement of students in the project, and the incorporation of this work in existing courses.Many computer-based scientific or engineering applications need to store, analyze, and manipulate large data. Often, this data has enough structure that specialized data structures and algorithms can have dramatically smaller memory and time requirements than explicit approaches. An important such case is symbolic verification of hardware and software, where, traditionally, binary decision diagrams (BDDs) have been successfully employed to study systems with enormous state spaces. Several software libraries for BDDs have arisen to support these operations, and BDDs have been applied to diverse applications as a means to exploit structure that is often hidden. However, in the past decade, decision diagram theory has continued to advance, by generalizing BDDs to variants with multi-way decisions (MDDs), multi-way or numerical outcomes, or edge values to encode real-valued data, and by proposing a variety of reduction rules to change (and often shrink) the decision diagram shape, as well as many important algorithmic improvements. Unfortunately, decision diagram libraries have not kept up with these theoretical advances. The proposed work seeks to fill this gap, by merging and expanding two existing prototype libraries developed by the two invesigators, Meddly and TEDDY, into a powerful, next-generation decision diagram library that supports a more general theory of decision diagrams. The new library will encompass (1) non-binary variables, including a-priori unbounded discrete domains and even infinite domains under certain restrictions, (2) non-boolean function values, attached either to terminal nodes or to the edges of the decision diagram, and (3) a more general definition of canonicitythat includes a wide spectrum of reduction rules. Several proposed activities will help smooth the learning curve for users adopting this library, from proven methods such as user manuals, tutorials, examples, wikis, and user groups, to novel ones such as the development of visualization techniques to aid the debugging and understanding of decision diagrams. The proposed software will push decision diagram library support far beyond the capabilities of today's typical BDD libraries, allowing exciting new applications to emerge in diverse fields well beyond classic ones such as symbolic model checking. Additionally, the proposed research activities will improve our understanding of decision diagram technology, providing deep new insights into the nature of structured functions and their representations. This has the potential to advance the state of the art both in fields that currently utilize decision diagrams, as improved library support can lead to the ability to tackle problem instances of unprecedented size, and in fields where the availability of a library implementing the proposed decision diagram variants will allow researchers to tackle classic problems with novel approaches based on decision diagrams. A next-generation decision diagram library will positively impact disciplines ranging from engineering to computer science theory to biology, via improved software applications that manage large and structured data. Letters of support attest to the many research groups worldwide eager to include more general and powerful decision diagram capabilities in their tools. The anticipated educational impact includes development of publicly available online tutorials; research, implementation, and experimentation opportunities for both undergraduate and graduate students; and integration of the developed techniques and software into existing courses via lectures, assignments, and projects. The underlying theory and developed software resulting from the proposed activities will reinforce concepts that students will retain and apply during their careers.

有各种各样的科学问题，其解决是困难的，因为必须考虑和评估的可能性非常多。通常，这种困难是由相互作用的组件的大量组合造成的，即使单个组件相对简单。相关的实际问题是测量通信网络的可靠性，其中链接可能会失败（由于网络中不同通信路径的数量而变得困难），或者确定汽车的刹车总是有效（由于汽车中相互作用的软件和硬件组件的组合数量而变得困难）。或者确定一台发电机的故障不会导致影响全国大部分电网的级联故障。这类问题在概念上类似于寻找魔方的最佳解决方案（这是由于大量不同的可能配置而变得困难），或者在国际象棋中，确定国际象棋中是否存在使白棋总是获胜的移动序列（由于大量不同的可能棋局而变得困难）。这个项目的目标是开发一个名为Meddly的软件库，各种应用程序可以使用它来构建和表示这些类型的组合问题的解决方案。Meddly的底层技术是决策图，这是一种组织数据的机制，可以在计算过程中自动发现和利用重复的模式或子模式。该项目将增加决策图技术的能力，有助于提高对该技术的理解，并将其应用于更多类型的问题。来自世界各地的一些研究人员对Meddly表示了兴趣，作为该项目的一部分，开发人员将帮助这些研究人员将Meddly集成到现有工具中，然后将其应用于实际问题。该项目还具有教育目标，通过学生参与该项目，并将此工作纳入现有课程。许多基于计算机的科学或工程应用程序需要存储、分析和操作大数据。通常，这些数据具有足够的结构，专用数据结构和算法比显式方法具有更小的内存和时间需求。其中一个重要的例子是硬件和软件的符号验证，传统上，二进制决策图（bdd）已经成功地用于研究具有巨大状态空间的系统。已经出现了一些用于bdd的软件库来支持这些操作，并且bdd已被应用于各种应用程序，作为一种利用通常隐藏的结构的手段。然而，在过去的十年中，决策图理论继续发展，通过将bdd推广到具有多路决策（mdd），多路或数值结果或边值的变体来编码实值数据，并提出各种约简规则来改变（通常是缩小）决策图形状，以及许多重要的算法改进。不幸的是，决策图库并没有跟上这些理论的发展。提议的工作旨在填补这一空白，通过合并和扩展两个由两位研究者Meddly和TEDDY开发的现有原型库，使其成为一个强大的下一代决策图库，支持更一般的决策图理论。新的库将包含(1)非二进制变量，包括先验的无界离散域，甚至在某些限制下的无限域，(2)非布尔函数值，附加到终端节点或决策图的边缘，以及(3)更一般的规范性定义，包括广泛的约简规则。一些建议的活动将帮助采用此库的用户平滑学习曲线，从用户手册、教程、示例、wiki和用户组等经过验证的方法，到开发可视化技术以帮助调试和理解决策图等新方法。所提议的软件将推动决策图库的支持远远超出当今典型的BDD库的能力，允许令人兴奋的新应用程序出现在不同的领域，远远超出经典的领域，如符号模型检查。此外，提出的研究活动将提高我们对决策图技术的理解，为结构化函数及其表示的本质提供深刻的新见解。这有可能推动当前使用决策图的领域的技术水平，因为改进的库支持可以导致处理空前规模的问题实例的能力，并且在实现所提议的决策图变体的库的可用性将允许研究人员使用基于决策图的新方法来解决经典问题的领域。下一代决策图库将通过改进的管理大型结构化数据的软件应用程序，对从工程到计算机科学理论到生物学等学科产生积极影响。支持信证明了世界各地的许多研究小组渴望在他们的工具中包含更通用和强大的决策图功能。预期的教育影响包括开发公开可用的在线教程；为本科生和研究生提供研究、实施和实验机会；通过讲座、作业和项目，将开发的技术和软件集成到现有的课程中。从所建议的活动中产生的基础理论和开发的软件将加强学生将在其职业生涯中保留和应用的概念。

项目成果

Reachability Set Generation Using Hybrid Relation Compatible Saturation

使用混合关系兼容饱和度生成可达性集

• DOI: 10.1007/978-3-030-61739-4_3
• 发表时间: 2020
• 期刊: Lecture notes in computer science
• 作者: Biswal, Shruti;Miner, Andrew S
• 通讯作者: Miner, Andrew S

SOUPS: A Variable Ordering Metric for the Saturation Algorithm

SOUPS：饱和算法的可变排序度量

• DOI: 10.1109/acsd.2018.000-4
• 发表时间: 2018
• 期刊: 2018 18th International Conference on Application of Concurrency to System Design (ACSD
• 作者: Smith, Benjamin;Ciardo, Gianfranco
• 通讯作者: Ciardo, Gianfranco

Variable Reordering in Binary Decision Diagrams

二元决策图中的变量重新排序

• 发表时间: 2017
• 期刊: 26th International Workshop on Logic & Synthesis
• 作者: Jiang, Chuan;Babar, Junaid;Ciardo, Gianfranco;Miner, Andrew S.;Smith, Benjamin
• 通讯作者: Smith, Benjamin

Improving Saturation Efficiency with Implicit Relations

利用隐式关系提高饱和效率

• DOI: 10.1007/978-3-030-21571-2_17
• 发表时间: 2019
• 期刊: International Conference on Applications and Theory of Petri Nets and Concurrency
• 作者: Biswal, Shruti;Miner, Andrew
• 通讯作者: Miner, Andrew

Generation of Minimum Tree-Like Witnesses for Existential CTL

存在 CTL 的最小树状见证的生成

• DOI: 10.1007/978-3-319-89960-2_18
• 发表时间: 2018
• 期刊: Tools and Algorithms for the Construction and Analysis of Systems
• 作者: Jiang, Chuan;Ciardo, Gianfranco
• 通讯作者: Ciardo, Gianfranco