Formal Specification and Model Checking of Dijkstra, A* and LPA* Algorithms

A small example

- example.maude         Observable component style of the systems specification of a simple example
- example-oo.maude    Object-oriented style of the systems specification of a simple example

Dijkstra

- dijkstra00.maude for DAG6
- dijkstra01.maude for DAG11
- dijkstra02.maude for DAG21
- dijkstra03.maude for DAG31
- dijkstra04.maude for DAG41
- dijkstra05.maude for DAG51

A*

- astar00.maude for DAG6
- astar01.maude for DAG11
- astar02.maude for DAG21
- astar03.maude for DAG31
- astar04.maude for DAG41
- astar05.maude for DAG51

LPA*

- lpastar00.maude for DAG6
- lpastar01.maude for DAG11
- lpastar02.maude for DAG21
- lpastar03.maude for DAG31
- lpastar04.maude for DAG41
- lpastar05.maude for DAG51

---

July 20, 2020; Oct 07, 2019 by ogata