Name
Abstract | ||
|---|---|---|
Hybrid logic refers to a group of logics lying between modal and first-order logic in which one can refer to individual states of the Kripke structure. In particular, the hybrid logic HL(@, ↓ ) is an appealing extension of modal logic that allows one to refer to a state by means of the given names and to dynamically create new names for a state. Unfortunately, as for the richer first-order logic, satisfiability for the hybrid logic HL(@, ↓ ) is undecidable and model checking for HL(@, ↓ ) is PSpace-complete. We carefully analyze these results and we isolate large fragments of HL(@, ↓ ) for which satisfiability is decidable and model checking is below PSpace. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11538363_24 | CSL |
Keywords | Field | DocType |
modal logic,model checking,large fragment,richer first-order logic,appealing extension,individual state,hybrid logic,new name,first-order logic,kripke structure | Hybrid logic,Discrete mathematics,Normal modal logic,Computer science,Multimodal logic,Decidability,First-order logic,Modal logic,Dynamic logic (modal logic),Intermediate logic | Conference |
Volume | ISSN | ISBN |
3634 | 0302-9743 | 3-540-28231-9 |
Citations | PageRank | References |
35 | 1.33 | 14 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Balder Ten Cate | 1 | 630 | 51.21 |
| Massimo Franceschet | 2 | 658 | 39.91 |