CirView: Visualization of LTL Path Checking Via Boolean Circuits

[2010-02-26, version 0.4, rev. c7f4e9d83ba7]

Introduction

CirView is a small tool for visualizing the construction and evaluation of
boolean circuits that represent the value of a formula in linear time temporal
logic (LTL) over a finite trace. A trace is an interpretation of the propositions
of the formula over the course of time. The circuits are visualized and
animated in 3D. The tool demonstrates the evaluation of a circuit using the
parallel contraction algorithm described in [KF09].
It is part of a larger library for investigating different evaluation
strategies and their implementation for boolean circuits for LTL path checking.
We will support the visualization of a broader range of evaluation strategies
from that library in the upcoming releases of the tool.

Publications

[KF09]

Lars Kuhtz and Bernd Finkbeiner. LTL Path Checking is Efficiently Parallelizable. ICALP 09, 2009.

Usage

For usage information call the tool as CirView --help.

The circuits are visualized via GLUT/openGL. We think the animation is
reasonably smooth. However, we have not optimized the rendering code.
Make sure you have hardware accelerated graphics and better not run the binary
remotely.

Documentation

The tool itself is quite verbose about its usage. If you have questions please contact Lars Kuhtz.

Download

You can download and use CirView under the terms of the following LICENSE.

Current version

0.4 [2010-03-05, rev. c7f4e9d83ba7, linux x86-64bit]

Contact

Lars Kuhtz <kuhtzXcsYuni-sbYde> (substitute X by @ and Y by .)