This tool (standing for *INference of Shortest Paths with EQuivalent Time-abstract behaviOR*)
is an implementation of the inverse method in the framework of Parametric Directed Weighted Graphs.

InSPEQTor takes as an input a Parametric Directed Weighted Graph, and a reference valuation for each parameter. It can synthesize two constraints on the weights of the graph seen as parameters:

- either a constraint guaranteeing the preservation of
**shortest paths**, or - a constraint guaranteeing the preservation of
**circuits of maximal mean**.

In the first case,
each **shortest path** in the graph instantiated with the reference valuation
is also a shortest path for any parameter valuation satisfying the constraint (and conversely).

In the second case (coming from the Max−Plus Algebra),
each **circuit of maximal mean** in the graph instantiated with the reference valuation
is also a circuit of maximal mean for any parameter valuation satisfying the constraint (and conversely).

InSPEQTor has been developed in OCaml by Étienne André in 2009-2010 at Laboratoire Spécification et Vérification, ENS Cachan, France. It is provided under the GNU-GPL license.

InSPEQTor takes as input a text file describing a Parametric Directed Weighted Graph, including the reference value for each parameter.

The syntax is described in a functional style, with OCaml-style (possibly nested) comments.

The call syntax is:

./INSPEQTOR [file.ins]

The result is given directly in the terminal.

By default, InSPEQTor synthesize constraints guaranteeing the preservation of shortest paths. To run InSPEQTor in order to synthesize constraints guaranteeing the preservation of circuits of maximal mean, use option -maxplus.

Version | Release | Source (tar.bz2) | Source (zip) | Binary |
---|---|---|---|---|

0.2 | 13th September 2010 | InSPEQTor.tar.bz2 (26Ko) | InSPEQTor.zip (34Ko) | INSPEQTOR (201Ko) |

0.1 | 25th May 2009 | − | − | − |

The binary is a standalone binary for Ubuntu; it has been compiled using Ubuntu 10.10. If it doesn’t work, please compile the source code.

Name | File |
---|---|

Toy example | exemple.ins |

Example from book "Initiation à l’algorithmique" p.551 | exLivralgo.ins |

Going from Place d’Italie to LSV | PlacedItalieLSV.ins |

Going from Rennes to LSV | RennesLSV.ins |

Going from Rennes to LSV (alternative version) | RennesLSV2.ins |

Going from Rennes to LSV (Ph.D. thesis manuscript version) | RennesLSVthese.ins |

- Étienne André (developer)

- Étienne André. An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems. Ph.D. thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2010. 268 pages. (English) [PDF | BibTeX | Slides]
- Étienne André and Laurent Fribourg. An Inverse Method for Policy-Iteration Based Algorithms. In Azadeh Farzan and Axel Legay (eds.), INFINITY’09, Electronic Proceedings in Theoretical Computer Science 10, pages 44–61, 2009. DOI: 10.4204/EPTCS.10.4 (English) [PDF (published version) | BibTeX | Slides]
- Étienne André. Une méthode inverse pour les plus courts chemins. ETR’09, 2009. (Français) [PDF | BibTeX | Slides]

This page makes use of valid HTML 5 and valid CSS.