Abstract | ||
---|---|---|
In this paper we apply answer set programming to solve alternating Boolean equation systems. We develop a novel characterization of solutions for variables in disjunctive and conjunctive Boolean equation systems. Based on this we devise a mapping from Boolean equation systems with alternating fixed points to normal logic programs such that the solution of a given variable of an equation system can be determined by the existence of a stable model of the corresponding logic program. The technique can be used to model check alternating formulas of modal μ-calculus. |
Year | DOI | Venue |
---|---|---|
2004 | 10.1007/11415763_9 | INAP/WLP |
Keywords | Field | DocType |
fixed point,corresponding logic program,conjunctive boolean equation system,stable model,normal logic program,boolean equation system,novel characterization,equation system,answer set programming,model checking | Maximum satisfiability problem,Boolean network,Data mining,Boolean circuit,Algebra,Computer science,Algorithm,Product term,Boolean algebra,Standard Boolean model,Boolean expression,And-inverter graph | Conference |
Volume | ISSN | ISBN |
3392 | 0302-9743 | 3-540-25560-5 |
Citations | PageRank | References |
2 | 0.37 | 15 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Misa Keinänen | 1 | 38 | 3.59 |
Ilkka Niemelä | 2 | 2939 | 148.38 |