Statische Teilauftragsreduzierung für einen gegebenen Zustandsraum

Question

Die meisten Veröffentlichungen zur Reduktion partieller Ordnung gehen davon aus, dass das zu analysierende System als eine Menge von Prozessen mit einem Zusammensetzungsoperator angegeben wird. Dies ist sehr sinnvoll, da Sie den Zustandsraum nicht zuerst berechnen und dann mit der Reduktion partieller Ordnung reduzieren möchten.

Aber unter der Annahme, dass Sie bereits einen flachen Zustandsraum angegeben haben, können Sie ihn dennoch reduzieren, indem Sie die Teilauftragsreduktion verwenden? Ich dachte, dass dies mit einem modifizierten DFS möglich sein sollte. Einige Eigenschaften können lokal geprüft werden, und die Zyklusbedingung kann berücksichtigt werden, indem die Informationen über Zustände auf dem Stapel verwendet werden.

Gibt es Papier oder eine andere Referenz, wo solch ein Algorithmus präsentiert wird?

Answer 1

Ja, das ist möglich. Wie Sie beschrieben haben, ist der Algorithmus dem traditionellen Ansatz sehr ähnlich. Der einzige Unterschied besteht darin, dass Informationen über die Unabhängigkeit von Aktionen gesammelt werden. Konzeptionell ist das alles ziemlich einfach. Daher glaube ich nicht, dass es irgendwelche Papiere zu einem solchen Algorithmus gibt.

Für Ihren Anwendungsfall ist eine Bisimulationsminimierung sinnvoller. Baier und Katoen geben eine großartige Einführung in ihr Buch "Principles of Model Checking". Der Stand der Technik wird in "Paige und Tarjan - Drei Partitionsverfeinerung Algorithmen" für starke Bisimulation und "Groote und Wijs - An O (m Log n) Algorithmus für Stottern Äquivalenz und Verzweigung Bisimulation" für die Verzweigung bisimulation beschrieben.