EST 2nd Edition


Project: Efficient Symbolic Tools - 2nd Edition

Synopsis: EST 2nd Edition is a toolbox for the formal verification of concurrent systems

Administrator: Robert Meolic (

Authors: Robert Meolic, Tatjana Kapus, Zmago Brezo─Źnik

History: started in 2000, first release in 2003

COBISS-ID: 5626902 (this number is used by Slovenian libraries)


[all] based on BDD package Biddy, includes API functions for Tcl/Tk GUI called My Interface, uses POSIX threads (currently disabled)

[pa] parser for simple textual representation of processes, encoding and decoding of processes, decoding of compositons, copying processes, process2composition, composition2process

[versis] parallel composition, multi-way parallel composition, checking strong equivalence, observational equivalence, testing equivalence, and trace equivalence, minimization with regard to strong, observational, and trace equivalence, renaming, hiding and forbiding actions, searching for deadlocks and divergences

[mc] ACTL model checking, ACTLW model checking based on EEU, EEG, AAW, and AAF, inevitable model checking, on-the-fly model checking, linear witnesses and counterexamples, diagnostic, witness and counterexample automata

[strucval] synchronous product of LTSs and witness/counterexample automata

[ccs] enhanced CCS parser, parser for Verilog netlists

. . .

EST 2nd Edition - release 6.x (last updated Oct 9, 2017)

New features

[all] output is now via sockets to support remode mode (e.g. WebEST)

[mc] ACTL/ACTLW formulae given in the file can have names

Other significant changes from release 5.7

[all] updated My Interface to 1.3

[all] updated Biddy (v1.7.3 is required for release 6.2)

[all] removed Makefiles for SunOS, linking simplified, without def files on MS Windows

[all] now, the same shared library is used with and without Tk GUI

[bdd] module bdd reorganized to support additional BDD types and additional BDD packages

[pa] BDD related part of pa module moved to bdd module

[pa] processes and compositions are never overwritted

[pa] a big improvement on state management and Pa_CopyProcess

[pa] a big improvement on counting states and transitions

[versis] improved parallel composition

Download sources, Oct 9, 2017, SVN revision 160, Jul 15, 2016, SVN revision 133, Sep 01, 2015, SVN revision 107

. . .

EST 2nd Edition - release 5.7 (Apr 25, 2015)

New features

[all] added main program (it can be used instead of wish)

[all] added cmdsh mode (tcl api without mish gui)

[bdd] added experimental drawing of BDDs using bddview

[pa] added reporting processes in FSP format (usable with LTSA tool)

[versis] implemented rename/hide/forbid of actions

[versis] implemented deadlock/divergent checking

[mc] model checker enhanced by Spin trail generation (usable with st2msc tool)

[mc] model checker enhanced by MSC generation (usable with mscgen tool)

Other significant changes from release 4.5

[all] updated My Interface to 1.1 (improved menus and xsource command)

[all] Biddy is isolated and does not belong to EST project anymore

[all] Biddy is now dynamically linked (v1.3 is required for release 5.7)

[all] modul gui added which covers functions removed in My Interface

[all] modul bdd added which covers functions removed in Biddy

[all] on MS Windows, bison, flex, and pthreads are now from MINGW distribution

[all] added Makefiles for MacOSX (Darwin)

[all] improved makefiles and packaging files, added debian and rpm packaging

[all] adapted for 64-bit architectures

[all] projects improved and cleaned

[all] examples improved and cleaned

[all] added documentation for examples

[all] now, Tcl Stubs are used everywhere (to support changes in Tcl 8.5.10)

[bdd] added Bdd_StabRS

[bdd] Bdd_RelOp, Bdd_RelOpSimple, and Bdd_RelOpComplex greatly improved

[pa] improved to produce usable result without explicitly enumeration of all transitions

[versis] improved parallel composition

[mc] fixed and greatly improved on-the-fly model checking for ACTL/ACTLW

[ccs] CCS parser improved

Download sources, Apr 25, 2015, SVN revision 104, Jun 20, 2014, SVN revision 86, Apr 29, 2013, SVN revision 78, Jul 6, 2012, SVN revision 64, May 16, 2012, SVN revision 55, Nov 01, 2010, SVN revision 43, Jun 20, 2008, SVN revision 37, Oct 18, 2007, SVN revision 35

. . .

EST 2nd Edition - release 4.5 (Jun 11, 2007)

New features

[mc] ACTL/ACTLW formulae can be read from file without starting model checker

[mc] ACTL/ACTLW formulae can use macros

[mc] added basic on-the-fly model checking for ACTL/ACTLW

[ccs] CCS parser extended to allow complex prefixes and action hiding ( [TAU/x] )

[ccs] CCS parser extended to support composition of minimized processes

[ccs] CCS parser extended to support minimization of composition

[ccs] CCS parser extended to support witness and counterexample automata

[ccs] CCS parser extended to support multi-way composition

[ccs] CCS parser extended to support on-the-fly model checking

[ccs] added parser for Verilog netlists

Other significant changes from release 3.5

[all] module ccs added

[all] bdd package becomes a separated project called Biddy

[all] mingw and sunos specific files removed, makefiles for Linux improved to support gcc v4

[all] examples and projects cleaned

[all] FSF rules to make program free are more strictly considered

[pa] counting states and transitions is now much faster

[pa] implemented smart encoding of processes

[pa] fixed renaming of processes

[versis] CCS parser fixed and more roboust

[versis] CCS parser moved from versis module to ccs module

[versis] fundamental-mode normalization changed

[versis] added step-by-step composition

[mc] added formula table

[mc] fixed diagnostic for AAW

[mc] added inevitable sets calculations for ACTL/ACTLW

Download sources, Jun 11, 2007, SVN revision 30, May 8, 2007, SVN revision 20, Jan 15, 2007, SVN revision 10, Oct 20, 2006, SVN revision 4, Oct 6, 2006, SVN revision 3, Jun 5, 2006

. . .

EST 2nd Edition - release 3.5 (Jun 12, 2006)

New features

[pa] processes can have final states

[pa] processes can be reported in CCS format

[versis] CCS parser extended with new composition types

[mc] strict ACTLW operators

[mc] witness and counterexample automata generation

[mc] minimization of WCA

[strucval] synchronous product

Other significant changes from release 2.2

[all] module strucval added

[all] improved dialogs

[all] makefiles improved, OS is now automaticaly recognized

[all] supported tcl/tk 8.4

[all] program sets unlimited stacksize (not working on Win32)

[all] threads are disabled

[all] functions using threads are now in separated files

[pa] fixed copying of processes

[pa] states, sorts and processes can be deleted

[pa] parser for process algebra is more roboust

[versis] CCS parser fixed

[versis] CCS parser improved, e.g. (a + b).P is now equal to a.P + b.P

[versis] composition of processes is simplified

[mc] semantics of standard ACTL fixed

[mc] precedence of Boolean and temporal operators fixed

[mc] HME and HMA are now strong version of HM operators

[mc] model checking is now based on strict ACTLW operators

[mc] ACTL/ACTLW formula can be given as a string parameter

[mc] parser for ACTL/ACTLW is more roboust

Download sources, Jun 12, 2006, May 26, 2006, Feb 2, 2006, Dec 19, 2005, Nov 16, 2005, Aug 03, 2004

. . .

EST 2nd Edition - release 2.2 (Feb 17, 2004)

New features

[versis] CCS parser

[mc] standard ACTL model checking

[mc] counterexamples and witnesses for standard ACTL operators

Other significant changes from release 2.0

[pa] states can be marked as deleted

[pa] encoding of processes is simplified

[pa] decoding of composed states improved

[pa] the maintaining of gates changed

[pa] option GATES removed from syntax of textual description of LTS

[pa] parser for textual description of LTS can now read the syntax from 1st Edition

[pa] parser for process algebra is now more roboust

[pa] added simple recovery on syntax errors

[versis] equivalences between processes with different sorts fixed

[versis] all minimizations greatly improved

[mc] semantics of ACTLW fixed

[mc] W is used instead of UU for unless

[mc] parser for ACTL/ACTLW is now more roboust

[mc] added simple recovery on syntax errors


est-2ed-2-2, Feb 17, 2004 (not available)
est-2ed-2-1, Sep 16, 2003 (not available)

. . .

EST 2nd Edition - release 2.0 (Aug 7, 2003)

This was the initial release of EST 2nd Edition. It was capable of representation of concurrent systems with LTSs, parallel composition of LTSs, multi-way parallel composition of LTSs, strong, observational testing and trace equivalence checking between LTSs, minimization of LTSs with regard to strong, observational, and trace equivalence, ACTLW model checking based on EEU, EEG, AAW, and AAF, and generation of counterexamples and witnesses.


est-2ed-2-0, Aug 7, 2003 (not available)

History notes

Project EST started in 1992 and version 1.0 was ready in 1999. We wanted to keep original branch of the package simple, because of its suitability of demonstrating the basic algorithms. Therefore, we made the copy of a package before introducing new features (September 2000). Original branch became EST 1st Edition while the new one is called EST 2nd Edition. Later, we made a lot of changes in data structures and algorithms of EST 2nd Edition and they become incompatible with the ones used in EST 1st Edition. Hence, modules from EST 1st Edition and EST 2nd Edition are not interchangeable.

In August, 2003, a release 2.0 was formed as a first official release of EST 2nd Edition. We started with number 2 to avoid the confusion with modules in EST 1st Edition.

From August 2003 until October 2006, EST 2nd Edition project used a CVS repository. In October 2006, we deleted it and created a SVN repository

Acknowledgement: Until now, the project EST 2nd Edition has been entirely realized during the research process on Faculty of Electrical Engineering and Computer Science in Maribor, Slovenia. We are collaborating with Formal Methods and Tools Group at ISTI in Pisa, Italy.

Published on  October 10th, 2017 - Robert Meolic, University of Maribor