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
Click here to go to my home page (in Italian).
hlmc [-h] | ([-l] [-s] <model_file>)Where:
||shows program usage and reference information|
||uses the MCLite procedure (otherwise MCFull is used)|
||prints evaluation statistics|
||is the name of the XML file, instance of the DTD hl-ks.dtd, containing the Kripke structure to use as model|
0if everything is OK, otherwise
1is returned (i.e., an error is occurred). The first line of
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_]
phi_01.hlfagainst the model
$ hlmc m.xml < phi_01.hlfTo check the formula
r & <pi2>(p | j)against the model
$ hlmc -l n.xml
r & <pi2>(p | j)
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-*.hlffiles contain samples formula expressed on
Model-01.xmlcontains the KS depicted in the slide no 38 of first class, while files from
formula-01-05.hlfcontain the five formulas introduced in slides 39 and 40. Other
formula-01-*.hlffiles present various examples of hybrid logics language primitives on the same KS.
In order to use this program, you need:
$ make all
$ make docThe DOC++ documentation will be generated in
$ ./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 b2The 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
See the source comment and the cited
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.
 Massimo Franceschet and Maarten de Rijke.
Model checking for hybrid logics (with an application to semistructured data)
Journal of Applied Logic, 2005.
 Massimo Franceschet and Balder ten Cate.
Hybrid Logics. ESSLLI 2004 Summer School Course Notes.