article

Proof systems for satisfiability in Hennessy-Milner logic with recursion

Author:

Kim G. LarsenAuthors Info & Claims

Theoretical Computer Science, Volume 72, Issue 2-3

Pages 265 - 288

https://doi.org/10.1016/0304-3975(90)90038-J

Published: 23 May 1990 Publication History

Abstract

No abstract available.

Cited By

View all

Taleb RHallé SKhoury R(2023)Uncertainty in runtime verificationComputer Science Review10.1016/j.cosrev.2023.10059450:COnline publication date: 1-Nov-2023
https://dl.acm.org/doi/10.1016/j.cosrev.2023.100594
Aceto LCassar IFrancalanza AIngólfsdóttir A(2023)On first-order runtime enforcement of branching-time propertiesActa Informatica10.1007/s00236-023-00441-960:4(385-451)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1007/s00236-023-00441-9
Le Brun MAttard DFrancalanza AAronis SBieniusa A(2021)Graft: general purpose raft consensus in ElixirProceedings of the 20th ACM SIGPLAN International Workshop on Erlang10.1145/3471871.3472963(2-14)Online publication date: 18-Aug-2021
https://dl.acm.org/doi/10.1145/3471871.3472963
Show More Cited By

Index Terms

Proof systems for satisfiability in Hennessy-Milner logic with recursion

Recommendations

Combining epistemic logic and hennessy-milner logic
Logic and Program Semantics

We define an epistemic logic for labelled transition systems by introducing equivalence relations for the agents on the states of the labelled transition system. The idea is that agents observe the dynamics of the system modulo their ability to ...
Proving Isomorphism of First-Order Logic Proof Systems in HOL
Monitorability for the Hennessy---Milner logic with recursion

We study $$\mu $$μ HML, a branching-time logic with least and greatest fixpoints, from a runtime verification perspective. The logic may be used to specify properties of programs whose behaviour may be expressed as a labelled transition system. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theoretical Computer Science

Theoretical Computer Science Volume 72, Issue 2-3

Special issue on the Thirteenth Colleque sur les Arbres en Alge`bre et en Programmation Nancy, March 1988

May 23, 1990

187 pages

ISSN:0304-3975

Editor:
M. Nivat
Univ. of Paris, Chevilly-Larue, France

Issue’s Table of Contents

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 23 May 1990

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

31
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Taleb RHallé SKhoury R(2023)Uncertainty in runtime verificationComputer Science Review10.1016/j.cosrev.2023.10059450:COnline publication date: 1-Nov-2023
https://dl.acm.org/doi/10.1016/j.cosrev.2023.100594
Aceto LCassar IFrancalanza AIngólfsdóttir A(2023)On first-order runtime enforcement of branching-time propertiesActa Informatica10.1007/s00236-023-00441-960:4(385-451)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1007/s00236-023-00441-9
Le Brun MAttard DFrancalanza AAronis SBieniusa A(2021)Graft: general purpose raft consensus in ElixirProceedings of the 20th ACM SIGPLAN International Workshop on Erlang10.1145/3471871.3472963(2-14)Online publication date: 18-Aug-2021
https://dl.acm.org/doi/10.1145/3471871.3472963
Aceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2021)An operational guide to monitorability with applications to regular propertiesSoftware and Systems Modeling (SoSyM)10.1007/s10270-020-00860-z20:2(335-361)Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s10270-020-00860-z
Attard DAceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2021)Better Late Than Never or: Verifying Asynchronous Components at RuntimeFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-030-78089-0_14(207-225)Online publication date: 14-Jun-2021
https://dl.acm.org/doi/10.1007/978-3-030-78089-0_14
Aceto LCassar IFrancalanza AIngólfsdóttir A(2021)On Bidirectional Runtime EnforcementFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-030-78089-0_1(3-21)Online publication date: 14-Jun-2021
https://dl.acm.org/doi/10.1007/978-3-030-78089-0_1
Castiglioni VChatzikokolakis KPalamidessi C(2020)A logical characterization of differential privacyScience of Computer Programming10.1016/j.scico.2019.102388188:COnline publication date: 1-Mar-2020
https://dl.acm.org/doi/10.1016/j.scico.2019.102388
Enevoldsen SLarsen KMariegaard ASrba J(2020)Dependency graphs with applications to verificationInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-020-00578-922:5(635-654)Online publication date: 1-Oct-2020
https://dl.acm.org/doi/10.1007/s10009-020-00578-9
Fahrenberg ULegay A(2020)Behavioral Specification Theories: An Algebraic TaxonomyLeveraging Applications of Formal Methods, Verification and Validation: Verification Principles10.1007/978-3-030-61362-4_14(262-274)Online publication date: 20-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-61362-4_14
Aceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2019)Adventures in monitorability: from branching to linear time and back againProceedings of the ACM on Programming Languages10.1145/32903653:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290365
Show More Cited By

Abstract

Cited By

Index Terms

Recommendations

Combining epistemic logic and hennessy-milner logic

Proving Isomorphism of First-Order Logic Proof Systems in HOL

Monitorability for the Hennessy---Milner logic with recursion

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations