A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F12%3A10125975" target="_blank" >RIV/00216208:11320/12:10125975 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/content/pdf/10.1007%2F978-3-642-31365-3_42" target="_blank" >http://link.springer.com/content/pdf/10.1007%2F978-3-642-31365-3_42</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-31365-3_42" target="_blank" >10.1007/978-3-642-31365-3_42</a>

Jazyk výsledku

angličtina

Název v původním jazyce

A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance

Popis výsledku v původním jazyce

Labelled superposition (LPSup) is a new calculus for PLTL. One of its distinguishing features, in comparison to other resolution-based approaches, is its ability to construct partial models on the fly. We use this feature to design a new decision procedure for the logic, where the models are effectively used to guide the search. On a representative set of benchmarks, our implementation is then shown to considerably advance the state of the art.

Název v anglickém jazyce

A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance

Popis výsledku anglicky

Labelled superposition (LPSup) is a new calculus for PLTL. One of its distinguishing features, in comparison to other resolution-based approaches, is its ability to construct partial models on the fly. We use this feature to design a new decision procedure for the logic, where the models are effectively used to guide the search. On a representative set of benchmarks, our implementation is then shown to considerably advance the state of the art.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2012

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Lecture Notes in Computer Science

ISSN

0302-9743

e-ISSN

—

Svazek periodika

2012

Číslo periodika v rámci svazku

7364

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

7

Strana od-do

537-543

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—