CirView: Visualization of LTL Path Checking Via Boolean Circuits
[2010-02-26, version 0.4, rev. c7f4e9d83ba7]
Coypright © 2010 Saarland Univerisity
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.
|[KF09]||Lars Kuhtz and Bernd Finkbeiner. LTL Path Checking is Efficiently Parallelizable. ICALP 09, 2009.|
For usage information call the tool as
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
The tool itself is quite verbose about its usage. If you have questions please contact Lars Kuhtz.
You can download and use CirView under the terms of the following LICENSE.
Lars Kuhtz <kuhtzXcsYuni-sbYde> (substitute X by @ and Y by .)