XTL (eXecutable Temporal Language) is a functional programming language interpreted over LTSs (Labelled Transition Systems) encoded in the BCG (Binary Coded Graph) file format. XTL can typically be used for implementing temporal logic operators, by describing their fixed point semantics as iterative or recursive computations over sets of states. More generally, XTL enables one to perform any computation on a BCG graph: for instance, it can compute the branching factor of a graph, print its list of labels, etc. XTL programs are compiled and evaluated on BCG graphs by using the xtl model checker.
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Evrard, Hugues; Lang, Frédéric: Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous (2017)
- Güdemann, Matthias; Salaün, Gwen; Ouederni, Meriem: Counterexample guided synthesis of monitors for realizability enforcement (2012)
- Garavel, Hubert; Lang, Frédéric; Mateescu, Radu; Serwe, Wendelin: CADP 2010: a toolbox for the construction and analysis of distributed processes (2011)
- Blom, Stefan; Orzan, Simona: Distributed branching bisimulation reduction of state spaces (2003)