## Abstract

Given a model M and a temporal logic formula phi[?], where ? is a placeholder. the query checking problem, as defined for the case of CTL by Chan in 2000, is to find the strongest propositional formula f such that M satisfies phi[? -> f]. The motivation for solving this problem is. among other things, to get insight on the model.

We consider various objectives to the LTL query-checking problem, and study the question of whether there is a better solution than simply enumerating all possible formulas (modulo logical equivalence). It turns out that in most cases the answer is no, but there is one particular objective for which the answer - in practice - is definitely yes. The solution is based on a reduction to a Pseudo-Boolean Solving problem.

Original language | English |
---|---|

Title of host publication | Hardware and Software: Verification and Testing |

Subtitle of host publication | 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers |

Editors | S Barner, Harris, D Kroening, O Raz |

Place of Publication | BERLIN |

Publisher | Springer-Verlag Berlin Heidelberg |

Pages | 76-92 |

Number of pages | 17 |

ISBN (Print) | 978-3-642-19582-2 |

DOIs | |

Publication status | Published - 2011 |

Event | 6th Haifa Verification Conference - Haifa, Israel Duration: 4 Oct 2010 → 7 Oct 2010 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | SPRINGER-VERLAG BERLIN |

Volume | 6504 |

ISSN (Print) | 0302-9743 |

### Conference

Conference | 6th Haifa Verification Conference |
---|---|

Country/Territory | Israel |

City | Haifa |

Period | 4/10/2010 → 7/10/2010 |