Hybrid Logics Model Checker

by Luigi Dragone [e-Mail] [Home Page]

Overview

This is a C implementation of model checking algorithms for Hybrid Logics MCLite and MCFull discussed in [1] and [2].

The model checker requires an Kripke structure for hybrid logics expressed as an XML file and a formula, it checks in which worlds, if any, of the provided model the formula holds.

The implementation relies on the XML parser Expat and the Peter Graf's PBL library. It is written using GNU GCC, but it can be compiled on Win32 platform using adequate tools (e.g., MinGW or Cygwin). Please refer to subsequent section for building instructions.

This software is released under GNU General Public License. It can be freely used, modified and distributed in conformity with the GNU General Public License. The License Agreement is available here. For any information about the GNU GPL and its implications please refer to GNU site.

The content of this site is provided "AS IS" without warranties of any kind either express or implied. Currently, I am working on to improve the performance (and correct its bug too). Please send me any comment or suggestion and report me any bug you notice. If you plan to employ this component in some application, please notice it me (this is not conforming to GNU GPL, but I would know if my work is useful).

To contact me please send an e-mail to luigi@luigidragone.com.
Click here to go to my home page (in Italian).

Change log

Usage instructions

In following sections basic usage instructions are provided. Please refer to cited papers for an introductions about hybrid logics and to Hybrid Logics' Home Page.

Command reference

This program reads a formula from the stdin and checks in which worlds of the given model the formula holds, writing them on stdout. It can be executed using a command line according to the following syntax:
    hlmc [-h] | ([-l] [-s] <model_file>)
Where:
-h
 shows program usage and reference information
-l
 uses the MCLite procedure (otherwise MCFull is used)
-s
 prints evaluation statistics
<model_file> is the name of the XML file, instance of the DTD hl-ks.dtd,  containing the Kripke structure to use as model
The exit code is 0 if everything is OK, otherwise 1 is returned (i.e., an error is occurred). The first line of
program output contains the list of model's worlds where the given formula holds, if the formula fails to be true on all the worlds, then the list is empty.

Formula syntax

The formula is read from the stdin and it is parsed according the following grammar:

formula ::= exp
exp 	::= id				prop. symbol, nominal or variable identifier
	| T				true constant
	| F				false constant
	| ! exp				not 
	| exp & exp			and 
	| exp '|' exp			or 
	| exp -> exp			implies
	| < id > ( exp )		diamond 
	| < id > - ( exp )		inverse diamond
	| [ id ] ( exp )		box 
	| [ id ] - ( exp )		inverse box
	| E exp				exists
	| A exp				for all
	| @ id ( exp )			at
	| B id ( exp )			bind variable
	| ( exp )
id 	::= [a-z_][a-zA-Z0-9_]

Kripke structure syntax

The structure against which the truth of the formula is checked is expressed as a Kripke structure for hybrid logics. These data are stored in XML files formatted according the DTD hl-ks.dtd.  Every element is identified by a label: since these attributes are XML ID different kinds of element cannot share the same label.
A Kripke structure file enumerates the worlds of the model, the modality access relations as world pairs. The truth assignment of propositional symbols is represented as the list of the world identifiers in which the symbol is true, it is assumed false in remaining others.The assignment of nominals is specified by the identifier of the corresponding world.
Please refer to DTD's comments and examples for more details about data format and structure.

Usage examples

To check the formula in file phi_01.hlf against the model m.xml:
$ hlmc m.xml < phi_01.hlf
To check the formula r & <pi2>(p | j) against the model n.xml using MCLite:
$ hlmc -l n.xml 
r & <pi2>(p | j) 
^Z

Test files

Test files in test/ directory are mainly based upon examples presented in the ESSLLI'04 hybrid logics classes held by Massimo Franceschet e Balder ten Cate.

Formula-00-*.hlf files contain samples formula expressed on model-00.xml.

Model-01.xml contains the KS depicted in the slide no 38 of first class, while files from formula-01-01.hlf to formula-01-05.hlf contain the five formulas introduced in slides 39 and 40. Other formula-01-*.hlf files present various examples of hybrid logics language primitives on the same KS.

System requirements

In order to use this program, you need:

To build this program on Win32 platform please consider to use MinGW 3.1 with MSYS 1.0. You need also to install Bison and Flex provided by GnuWin32
For convenience a sample makefile for Win32 platform is included, please adjust path to actual library installation locations accordingly.

Build instructions

  1. Download and install the required libraries and tools (compiling them, if required)
  2. Set up system search path for header and library files
  3. Download the source distribution and unpack it
  4. Configure the Makefile accordingly
  5. To build the program please run from the source's root directory: 
    $ make all
  6. (optional step) To compile the documentation hypertext please run:
    $ make doc
    The DOC++ documentation will be generated in doc/ subdir
  7. (optional) To check the program please run it against some formulas in test/ subdir. Ex.: 
    $ ./hlmc test/model-01.xml < test/formula-01-04.hlf

root_node index_node b1 b2 a1 a11 a12 t1 a21 t2 d2 a31 t3 d3 

$ ./hlmc test/model-01.xml < test/formula-01-05.hlf


$ ./hlmc test/model-01.xml < test/formula-01-20.hlf

b2
    The first one should be checked as valid (the formula is satisfied in every model's worlds), while the second should be reported as unsatisfiable. The third one holds only in the world b2.

Documentation

See the source comment and the cited references for specific details about the algorithm and its implementation. The source code is annotated with algorithm's pseudo code as formulated in ESSLLI's course notes.
Public data structures and functions are also annotated with DOC++ comments.

References

[1] 	Massimo Franceschet and Maarten de Rijke. 
	Model checking for hybrid logics (with an application to semistructured data)
  	Journal of Applied Logic, 2005.
[2] 	Massimo Franceschet and Balder ten Cate.
 	Hybrid Logics. ESSLLI 2004 Summer School Course Notes.

luigi@luigidragone.com.