 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||
| |||||||||||||||||||||
| |||||||||||||||||||||
|
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Einschränkung auf universelle Pfadquantoren |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
Viele der Methoden zur Vermeidung des Problems der Zustandsexplosion basieren auf kompositionellem Beweisen und Abstraktion. Die dafür typischerweise verwendete Logik enthält ausschließlich universelle Pfadquantoren.
Um schließlich durch diese Einschränkungen die Ausdrucksmächtigkeit der Logik nicht zu verringern, werden Konjunktion und Disjunktion sowie die temporalen Operatoren U und R benötigt. Beispiele von ACTL-Formeln sind AF AG a und AF AX a. Diese Formeln können nicht in LTL ausgedrückt werden. Da ACTL eine Untermenge von CTL ist, sind die Logiken ACTL und LTL nicht vergleichbar. ACTL* ist außerdem ausdrucksstärker als LTL. Die ACTL*-Formeln AG EF Start und AG ¬AF Start sind beispielsweise nicht in ACTL enthalten. Rückkehr zu Temporale Logik | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Einschränkung auf universelle... | ||||
| ||||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
