Maximal synthesis for Hennessy-Milner logic with the box modality

A.C. van Hulst; M.A. Reniers; W.J. Fokkink

doi:10.3182/20140514-3-FR-4046.00034

Maximal synthesis for Hennessy-Milner logic with the box modality

A.C. van Hulst, M.A. Reniers, W.J. Fokkink

Research output: Contribution to journal › Conference article › peer-review

2 Citations (Scopus)

Abstract

This paper presents a novel approach to adapt a behavioral model in order to satisfy a requirement in Hennessy-Milner Logic, including an additional box modality operator, expressing an invariant formula. Control system synthesis, as defined in this way, retains all non-invalidating behavior, and thereby guarantees maximal permissiveness for supervisory control. This research extends earlier work by embracing a broader synthesized logic, enabling synthesis with respect to invariant formulas for non-deterministic behavioral models. All definitions and proofs in this paper have been computer verified using the Coq proof assistant.

Original language	English
Pages (from-to)	278-285
Number of pages	8
Journal	IFAC Proceedings Volumes
Volume	47
Issue number	2
DOIs	https://doi.org/10.3182/20140514-3-FR-4046.00034
Publication status	Published - 2014
Event	12th International Workshop on Discrete Event Systems (WODES 2014) - Cachan, France Duration: 14 May 2014 → 16 May 2014 Conference number: 12 http://wodes2014.lurpa.ens-cachan.fr/

Keywords

Control system synthesis
Invariants
Supervisory control
Temporal logic

Access to Document

10.3182/20140514-3-FR-4046.00034

Cite this

@article{ea80e5e9b1954642a33318fc2d84576f,

title = "Maximal synthesis for Hennessy-Milner logic with the box modality",

abstract = "This paper presents a novel approach to adapt a behavioral model in order to satisfy a requirement in Hennessy-Milner Logic, including an additional box modality operator, expressing an invariant formula. Control system synthesis, as defined in this way, retains all non-invalidating behavior, and thereby guarantees maximal permissiveness for supervisory control. This research extends earlier work by embracing a broader synthesized logic, enabling synthesis with respect to invariant formulas for non-deterministic behavioral models. All definitions and proofs in this paper have been computer verified using the Coq proof assistant.",

keywords = "Control system synthesis, Invariants, Supervisory control, Temporal logic",

author = "{van Hulst}, A.C. and M.A. Reniers and W.J. Fokkink",

year = "2014",

doi = "10.3182/20140514-3-FR-4046.00034",

language = "English",

volume = "47",

pages = "278--285",

journal = "IFAC Proceedings Volumes",

issn = "1474-6670",

publisher = "Elsevier",

number = "2",

note = "12th International Workshop on Discrete Event Systems (WODES 2014), WODES 2014 ; Conference date: 14-05-2014 Through 16-05-2014",

url = "http://wodes2014.lurpa.ens-cachan.fr/",

}

TY - JOUR

T1 - Maximal synthesis for Hennessy-Milner logic with the box modality

AU - van Hulst, A.C.

AU - Reniers, M.A.

AU - Fokkink, W.J.

N1 - Conference code: 12

PY - 2014

Y1 - 2014

N2 - This paper presents a novel approach to adapt a behavioral model in order to satisfy a requirement in Hennessy-Milner Logic, including an additional box modality operator, expressing an invariant formula. Control system synthesis, as defined in this way, retains all non-invalidating behavior, and thereby guarantees maximal permissiveness for supervisory control. This research extends earlier work by embracing a broader synthesized logic, enabling synthesis with respect to invariant formulas for non-deterministic behavioral models. All definitions and proofs in this paper have been computer verified using the Coq proof assistant.

AB - This paper presents a novel approach to adapt a behavioral model in order to satisfy a requirement in Hennessy-Milner Logic, including an additional box modality operator, expressing an invariant formula. Control system synthesis, as defined in this way, retains all non-invalidating behavior, and thereby guarantees maximal permissiveness for supervisory control. This research extends earlier work by embracing a broader synthesized logic, enabling synthesis with respect to invariant formulas for non-deterministic behavioral models. All definitions and proofs in this paper have been computer verified using the Coq proof assistant.

KW - Control system synthesis

KW - Invariants

KW - Supervisory control

KW - Temporal logic

UR - http://www.scopus.com/inward/record.url?scp=84951832084&partnerID=8YFLogxK

U2 - 10.3182/20140514-3-FR-4046.00034

DO - 10.3182/20140514-3-FR-4046.00034

M3 - Conference article

AN - SCOPUS:84945932771

SN - 1474-6670

VL - 47

SP - 278

EP - 285

JO - IFAC Proceedings Volumes

JF - IFAC Proceedings Volumes

IS - 2

T2 - 12th International Workshop on Discrete Event Systems (WODES 2014)

Y2 - 14 May 2014 through 16 May 2014

ER -

Maximal synthesis for Hennessy-Milner logic with the box modality

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this