Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments

2016 ◽  
pp. 389-405 ◽  
Author(s):  
Laura Bozzelli ◽  
Alberto Molinari ◽  
Angelo Montanari ◽  
Adriano Peron ◽  
Pietro Sala
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Logic Model ◽  
Interval Temporal Logic ◽  
Logic Model Checking

UTP and Temporal Logic Model Checking

2010 ◽  
pp. 22-41 ◽  
Author(s):  
Hugh Anderson ◽  
Gabriel Ciobanu ◽  
Leo Freitas
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Logic Model ◽  
Logic Model Checking

Symmetry in temporal logic model checking

2006 ◽  
Vol 38 (3) ◽  
pp. 8 ◽  
Author(s):  
Alice Miller ◽  
Alastair Donaldson ◽  
Muffy Calder
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Logic Model ◽  
Logic Model Checking

Temporal Logic Model Checking

2005 ◽  
pp. 539-558 ◽  
Author(s):  
Edmund Clarke ◽  
Ansgar Fehnker ◽  
Sumit Kumar Jha ◽  
Helmut Veith
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Logic Model ◽  
Logic Model Checking

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