Computing sufficient and necessary conditions in CTL: a forgetting approach
R Feng, E Acar, Y Wang, W Liu, S Schlobach… - Information Sciences, 2022 - Elsevier
Computation tree logic (CTL) is an essential specification language in the field of formal
verification. In systems design and verification, it is often important to update existing …
verification. In systems design and verification, it is often important to update existing …
Common equivalence and size of forgetting from Horn formulae
P Liberatore - Annals of Mathematics and Artificial Intelligence, 2024 - Springer
Forgetting variables from a propositional formula may increase its size. Introducing new
variables is a way to shorten it. Both operations can be expressed in terms of common …
variables is a way to shorten it. Both operations can be expressed in terms of common …
Knowledge forgetting in propositional μ-calculus
R Feng, Y Wang, R Qian, L Yang, P Chen - Annals of Mathematics and …, 2023 - Springer
The μ-calculus is one of the most important logics describing specifications of transition
systems. It has been extensively explored for formal verification in model checking due to its …
systems. It has been extensively explored for formal verification in model checking due to its …
The ghosts of forgotten things: A study on size after forgetting
P Liberatore - arXiv preprint arXiv:2005.04123, 2020 - arxiv.org
Forgetting is removing variables from a logical formula while preserving the constraints on
the other variables. In spite of being a form of reduction, it does not always decrease the size …
the other variables. In spite of being a form of reduction, it does not always decrease the size …
Common equivalence and size after forgetting
P Liberatore - arXiv preprint arXiv:2006.11152, 2020 - arxiv.org
Forgetting variables from a propositional formula may increase its size. Introducing new
variables is a way to shorten it. Both operations can be expressed in terms of common …
variables is a way to shorten it. Both operations can be expressed in terms of common …
Four algorithms for propositional forgetting
P Liberatore - arXiv preprint arXiv:2204.06528, 2022 - arxiv.org
Four algorithms for propositional forgetting are compared. The first performs all possible
resolutions and deletes the clauses containing a variable to forget. The second forgets a …
resolutions and deletes the clauses containing a variable to forget. The second forgets a …
Reconstructing a single-head formula to facilitate logical forgetting
P Liberatore - Journal of Logic and Computation, 2023 - academic.oup.com
Logical forgetting is removing some variables from a formula while maintaining its
consequences on the remaining variables. This removal may require exponential time on …
consequences on the remaining variables. This removal may require exponential time on …
[PDF][PDF] On Forgetting in CTL and Its Applications
R Feng, E Acar, S Schlobach, Y Wang, W Liu - researchgate.net
Computation tree logic (CTL) as a temporal logic, is one of the most common specification
languages in the field of formal verification. Typically, three cases are considered from both …
languages in the field of formal verification. Typically, three cases are considered from both …
[HTML][HTML] The ghosts of forgotten things: A study on size after forgetting
P Liberatore - Annals of Pure and Applied Logic, 2024 - Elsevier
Forgetting is removing variables from a logical formula while preserving the constraints on
the other variables. In spite of reducing information, it does not always decrease the size of …
the other variables. In spite of reducing information, it does not always decrease the size of …