Product Details
dWiNA - An Implementation of Decision Procedure for WS1S
Created: 2015
Czech title
dWiNA - Implementace rozhodovací procedury pro WS1S
Type
software
License
required - free
Authors
Fiedor Tomáš, Ing., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords
antichains
WS1S
finite automata
subsumption
nondeterministic automata
Description
This tool is an implementation of novel approach based on anti-chains for deciding Weak Monadic Second-Order Logic of one successor (WS1S).
Location
The tool and manual is located at
Licence
Free software under the terms of GNU GPL (cf.http://www.gnu.org/licenses/gpl.html).
Projects
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures (GA14-11384S)
Reliability and Security in IT (FIT-S-14-2486)
The IT4Innovations Centre of Excellence (ED1.1.00/02.0070)
Verification of Infinite State Systems Based on Finite Automata (GP13-37876P)
Reliability and Security in IT (FIT-S-14-2486)
The IT4Innovations Centre of Excellence (ED1.1.00/02.0070)
Verification of Infinite State Systems Based on Finite Automata (GP13-37876P)
Research groups
Departments
Department of Intelligent Systems FIT BUT (DITS FIT BUT)