scholarly journals Specification of Synchronous Network Flooding in Temporal Logic

2020 ◽  
Vol 17 (6) ◽  
pp. 867-874
Author(s):  
Ra’ed Bani Abdelrahman ◽  
Rafat Alshorman ◽  
Walter Hussak ◽  
Amitabh Trehan
Keyword(s):  
Temporal Logic ◽  
Network Topology ◽  
Distributed Network ◽  
Model Checker ◽  
Fixed Size ◽  
Network Algorithms ◽  
Worked Example ◽  
Synchronous Network ◽  
Termination Problem ◽  
Network Flooding

In distributed network algorithms, network flooding algorithm is considered one of the simplest and most fundamental algorithms. This research specifies the basic synchronous memory-less network flooding algorithm where nodes on the network don’t have memory, for any fixed size of network, in Linear Temporal Logic. The specification can be customized to any single network topology or class of topologies. A specification of the termination problem is formulated and used to compare different topologies for earlier termination. This research gives a worked example of one topology resulting in earlier termination than another, for which we perform a formal verification using the model checker NuSMV

scholarly journals A Topological Perspective on Distributed Network Algorithms

2019 ◽  
pp. 3-18 ◽  
Author(s):  
Armando Castañeda ◽  
Pierre Fraigniaud ◽  
Ami Paz ◽  
Sergio Rajsbaum ◽  
Matthieu Roy ◽  
...  
Keyword(s):  
Distributed Network ◽  
Network Algorithms

A non-communication methodology for distributed network topology recognition

2017 ◽  
Author(s):  
B.M. Keune ◽  
U. Luhring ◽  
C. Rehtanz ◽  
F. Jenau ◽  
J. Morales ◽  
...  
Keyword(s):  
Network Topology ◽  
Distributed Network

scholarly journals Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives

2013 ◽  
Vol 2013 ◽  
pp. 1-12 ◽  
Author(s):  
Rui Wang ◽  
Wanwei Liu ◽  
Tun Li ◽  
Xiaoguang Mao ◽  
Ji Wang
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Bounded Model Checking ◽  
Symbolic Model Checking ◽  
Model Checker ◽  
Symbolic Model ◽  
Complementary Technique

As a complementary technique of the BDD-based approach, bounded model checking (BMC) has been successfully applied to LTL symbolic model checking. However, the expressiveness of LTL is rather limited, and some important properties cannot be captured by such logic. In this paper, we present a semantic BMC encoding approach to deal with the mixture ofETLfandETLl. Since such kind of temporal logic involves both finite and looping automata as connectives, all regular properties can be succinctly specified with it. The presented algorithm is integrated into the model checker ENuSMV, and the approach is evaluated via conducting a series of imperial experiments.

Winning Strategy Tree Construction for BDD-Based ATL Model Checkers

2020 ◽  
Vol 30 (04) ◽  
pp. 555-573
Author(s):  
Wonhong Nam ◽  
Haejin Yang ◽  
Hyunyoung Kil
Keyword(s):  
Temporal Logic ◽  
Open System ◽  
Open Systems ◽  
Winning Strategy ◽  
Decision Diagrams ◽  
Model Checker ◽  
Binary Decision ◽  
Counter Example ◽  
Tree Construction ◽  
System Verification

The Alternating-time Temporal Logic (ATL) is a temporal logic for formal verification of open systems, which supports selective quantification over paths. The open system can be represented as a game where the system and the environment pick their moves in turn or simultaneously. The ATL model checker Mocha has been developed by using Binary Decision Diagrams (BDDs), and successfully employed for open system verification. However, since Mocha symbolically manipulates a set of states by a BDD, it is hard to generate a winning strategy as a witness or a counter-example. In this paper, we propose a novel algorithm to efficiently construct a winning strategy tree and report that our technique has been successfully implemented on Mocha.

Using Model Checking in a Parallelizing Compiler

1998 ◽  
Vol 08 (04) ◽  
pp. 459-471 ◽  
Author(s):  
Teodor Rus ◽  
Eric van Wyk
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Logic Model ◽  
Data Dependence ◽  
Parallelizing Compiler ◽  
Model Checker ◽  
Source Program ◽  
Formal Framework ◽  
Sequential Processes ◽  
Logic Model Checking

In this paper we describe the usage of temporal logic model checking in a parallelizing compiler to analyze the structure of a source program and locate opportunities for optimization and parallelization. The source program is represented as a process graph in which the nodes are sequential processes and the edges are control and data dependence relationships between the computations at the nodes. By labeling the nodes and edges with descriptive atomic propositions and by specifying the conditions necessary for optimizations and parallelizations as temporal logic formulas, we can use a model checker to locate nodes of the process graph where particular optimizations can be made. To discover opportunities for new optimizations or modify existing ones in this parallelizing compiler, we need only specify their conditions as temporal logic formulas; we do not need to add to or modify the code of the compiler. This greatly simplifies the process of locating optimization and parallelization opportunities in the source program and makes it easier to experiment with complex optimizations. Hence, this methodology provides a convenient, concise, and formal framework in which to carry out program optimizations by compilers.

Sign in / Sign up

Export Citation Format

Share Document