---
title: "A semantically-derived subset of English for hardware verification"
description: "The paper looks at how to turn English hardware specifications into CTL, the branching-time temporal… 19 references, cited by 3 papers here."
authors: ["Alexander Holt", "Ewan Klein"]
year: 1999
venue: "Proceedings of the 37th Annual Meeting of the Association for Computational Linguistics"
source: "https://aclanthology.org/P99-1058/"
doi: "10.3115/1034678.1034747"
licence: "CC BY-NC-SA 3.0 (ACL Anthology, before 2016)"
licence_url: "https://creativecommons.org/licenses/by-nc-sa/3.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/holt-1999-semantically-derived-subset-english-hardware/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/holt-1999-semantically-derived-subset-english-hardware/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [1999](https://md.research.elamur.ai/free/en/papers/1999/) / A semantically-derived subset of English for hardware verification

# A semantically-derived subset of English for hardware verification

**Authors:** Alexander Holt and Ewan Klein · **Year:** 1999 · **Venue:** [Proceedings of the 37th Annual Meeting of the Association for Computational Linguistics](https://md.research.elamur.ai/free/en/venues/acl/) ([ACL 1999](https://md.research.elamur.ai/free/en/venues/acl/1999/)) · **Publisher:** [Association for Computational Linguistics](https://md.research.elamur.ai/free/en/publishers/association-for-computational-linguistics/) · **Licence:** [CC BY-NC-SA 3.0 (ACL Anthology, before 2016)](https://creativecommons.org/licenses/by-nc-sa/3.0/)

**Links:** [Publisher's page](https://aclanthology.org/P99-1058/) · [PDF](https://aclanthology.org/P99-1058.pdf) · [DOI 10.3115/1034678.1034747](https://doi.org/10.3115/1034678.1034747) · [OpenAlex](https://openalex.org/W2118215721)

**Citations:** 30 citations (OpenAlex, 2026-10-14) · 3 in our library, of the 149,439 papers whose bibliographies we read

## Summary
The paper looks at how to turn English hardware specifications into CTL, the branching-time temporal logic used for model checking. The central difficulty is ensuring that every sentence a user may write actually has a CTL translation. Many earlier systems start from a general semantic analysis of English and then map it onto the target logic. The authors reverse this. They start from the limited expressive power of CTL and derive restricted subsets of English from it.

Their resources and tools are:
- a corpus of about a hundred specification sentences, elicited by asking qualified people to describe timing diagrams;
- a prototype parser built on a simplified Alvey grammar;
- a DCG generator, ctl2eng, which writes CTL formulas out as literal English.

The set of sentences ctl2eng can produce defines the lowest controlled language. Higher levels add synonyms, event vocabulary such as "rise" and "pulse", and finally phrasings that need inference to translate. The result is a hierarchy of sublanguages ordered by how closely they match CTL. The paper reports no accuracy figures. Its value is a principled way to design controlled languages that guarantees translatability.

## Key points
- CTL operators covered: AG (on all paths, always), AF (on all paths, eventually), AX (on all paths, at the next state) and A[f U g] (f holds on all paths until g becomes true).
- The data are about 100 English sentences describing timing diagrams, such as a pulsing circuit and a handshaking protocol. Respondents wrote both abstract and near-literal descriptions of the same behaviour.
- The prototype uses the Alvey Natural Language Tools Grammar, a GPSG-style grammar that produces event-based, unscoped semantics. The authors cut down its lexicon, reduced its coordination rules and dropped deontic readings of modals.
- The hierarchy has five levels:
  - L1 is the canonical transliteration, defined as the range of ctl2eng.
  - L1+ adds near-synonymous wording and maps to pure CTL.
  - L2 is compositional but uses a richer ontology. It maps to an extended CTL with predicates rise(p), fall(p) and pulse(p, v, n).
  - L2+ fixes the grammatical defects of L2 and adds some anaphora and ellipsis.
  - L3 is non-compositional, needing domain or temporal inference, and may require a full semantic representation.
- A context-free grammar approximates L2. Anaphora is not yet resolved. The authors plan to use the specification patterns of Dwyer et al. as further constraints on the controlled English.

## Interesting ideas
- The controlled language is defined as the output of a generator running from the formal language back to English, so every allowed sentence has a translation by construction.
- Inputs are graded by their semantic distance from the target formalism: direct transliteration, compositional but with a richer ontology, and needing inference.
- Event words like "edge" and "pulse" are treated as macros that expand into sequences of primitive state changes over successive time points.
- Some readings depend on domain conventions, for example "eventually" in a handshake protocol needing an extra next-step operator. The paper argues these conventions must be built in so that users can still predict how the system will react.
- Generated canonical sentences quickly become structurally ambiguous. The authors propose either generating unambiguous paraphrases or making the parser return every relevant reading.

## For Mova

How these ideas could serve Mova, our small open language model — its files, stages and tests:

- **I1** (back): Sentences generated from meaning graphs could form a "guaranteed round-trip" sublanguage, which would be a clean baseline test set for the text → graph → text compressor.
- **I2** (answer): Labelling each test sentence or question with such a level would separate failures caused by the parser from failures caused by missing inference, which makes evaluation more diagnostic.
- **I3** (world): Verbs of change (rise, fall, become, change) could be compiled into explicit before/after state patterns on the event timeline, which keeps them explainable.
- **I4** (frames): Domain-specific interpretation conventions should be stored as named, inspectable rules attached to a frame, not buried in the mapping, so each answer can cite the convention it used.
- **I5** (back): Mova's generator could check each output by reparsing it and rephrasing whenever more than one graph comes back.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [University of Edinburgh](https://md.research.elamur.ai/free/en/universities/university-of-edinburgh/) — University, Edinburgh, United Kingdom · 381 works · 80,747 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 321 works

🧭 Topics (2): [English](https://md.research.elamur.ai/free/en/topics/english/) · 2,379 works · [⚡ GPU & parallel computing](https://md.research.elamur.ai/free/en/topics/gpu-parallel-computing/) · 41 works

## Cite

Cite as: Alexander Holt and Ewan Klein. 1999. A semantically-derived subset of English for hardware verification. Proceedings of the 37th Annual Meeting of the Association for Computational Linguistics.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{holt1999semantically,
  title = {{A semantically-derived subset of English for hardware verification}},
  author = {Alexander Holt and Ewan Klein},
  booktitle = {Proceedings of the 37th Annual Meeting of the Association for Computational Linguistics},
  year = {1999},
  doi = {10.3115/1034678.1034747},
  url = {https://doi.org/10.3115/1034678.1034747}
}
```

- [← previous Using Coreference for Question Answering](https://md.research.elamur.ai/free/en/papers/morton-1999-coreference-question-answering/)
- [next → What is coreference, and what should coreference annotation be?](https://md.research.elamur.ai/free/en/papers/deemter-1999-what-is-coreference-what-should/)
- [↑ back to papers of 1999](https://md.research.elamur.ai/free/en/papers/1999/)

## References

19 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Hiyan Alshawi, editor. 1992. The Core Language Engine. MIT Press. [find](https://scholar.google.com/scholar?q=Hiyan+Alshawi%2C+editor%2E+1992%2E+The+Core+Language+Engine%2E+MIT+Press%2E)
2. Edmund M. Clarke and E. Allen Emerson. 1981. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, volume 131 of Lecture Notes in Computer Science. Springer-Verlag. [find](https://scholar.google.com/scholar?q=Edmund+M%2E+Clarke+and+E%2E+Allen+Emerson%2E+1981%2E+Synthesis+of+synchronization+skeletons+for+branching+time+temporal+logic%2E+In+Logic+of+Programs%3A+Workshop%2C+Yorktown+Heights%2C+NY%2C+May+1981%2C+volume+131+of+Lec)
3. Edmund M. Clarke and Jeanette M. Wing. 1996. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626-643. [find](https://scholar.google.com/scholar?q=Edmund+M%2E+Clarke+and+Jeanette+M%2E+Wing%2E+1996%2E+Formal+methods%3A+State+of+the+art+and+future+directions%2E+ACM+Computing+Surveys%2C+28%284%29%3A626%2D643%2E)
4. Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263. [find](https://scholar.google.com/scholar?q=Edmund+M%2E+Clarke%2C+E%2E+Allen+Emerson%2C+and+A%2E+Prasad+Sistla%2E+1986%2E+Automatic+verification+of+finite%2Dstate+concurrent+systems+using+temporal+logic+specifications%2E+ACM+Transactions+on+Programming+Languages)
5. Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. 1998a. Patterns in property specifications for finite-state verification. Technical Report KSU CIS TR-98-9, Department of Computing and Information Sciences, Kansas State University. [find](https://scholar.google.com/scholar?q=Matthew+B%2E+Dwyer%2C+George+S%2E+Avrunin%2C+and+James+C%2E+Corbett%2E+1998a%2E+Patterns+in+property+specifications+for+finite%2Dstate+verification%2E+Technical+Report+KSU+CIS+TR%2D98%2D9%2C+Department+of+Computing+and+Infor)
6. Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. 1998b. Property specification patterns for finite-state verification. In M. Ardis, editor, Proceedings of the Second Workshop on Formal Methods in Software Practice, pages 7-15. [find](https://scholar.google.com/scholar?q=Matthew+B%2E+Dwyer%2C+George+S%2E+Avrunin%2C+and+James+C%2E+Corbett%2E+1998b%2E+Property+specification+patterns+for+finite%2Dstate+verification%2E+In+M%2E+Ardis%2C+editor%2C+Proceedings+of+the+Second+Workshop+on+Formal+Metho)
7. A. Fantechi, S. Gnesi, G. Ristori, M. Carenini, M. Marino, and P. Moreschini. 1994. Assisting requirement formalization by means of natural language translation. Formal Methods in System Design, 4:243-263. [find](https://scholar.google.com/scholar?q=A%2E+Fantechi%2C+S%2E+Gnesi%2C+G%2E+Ristori%2C+M%2E+Carenini%2C+M%2E+Marino%2C+and+P%2E+Moreschini%2E+1994%2E+Assisting+requirement+formalization+by+means+of+natural+language+translation%2E+Formal+Methods+in+System+Design%2C+4%3A243)
8. Kathryn Fisler. 1996. A Unified Approach to Hardware Verification through a Heterogeneous Logic of Design Diagrams. Ph.D. thesis, Department of Computer Science, Indiana University. [find](https://scholar.google.com/scholar?q=Kathryn+Fisler%2E+1996%2E+A+Unified+Approach+to+Hardware+Verification+through+a+Heterogeneous+Logic+of+Design+Diagrams%2E+Ph%2ED%2E+thesis%2C+Department+of+Computer+Science%2C+Indiana+University%2E)
9. Norbert E. Fuchs and Rolf Schwitter. 1996. [Attempto Controlled English (ACE)](https://md.research.elamur.ai/free/en/papers/fuchs-1996-attempto-controlled-english-ace/). In CLAW 96: First International Workshop on Controlled Language Applications. Centre for Computational Linguistics, Katholieke Universiteit Leuven, Belgium.
10. Claire Grover, John Carroll, and Ted Briscoe. 1993. The Alvey Natural Language Tools Grammar (4th release). Technical Report 284, Computer Laboratory, University of Cambridge. [find](https://scholar.google.com/scholar?q=Claire+Grover%2C+John+Carroll%2C+and+Ted+Briscoe%2E+1993%2E+The+Alvey+Natural+Language+Tools+Grammar+%284th+release%29%2E+Technical+Report+284%2C+Computer+Laboratory%2C+University+of+Cambridge%2E)
11. Hans Kamp and Uwe Reyle. 1993. From Discourse to Logic: Introduction to Modeltheoretic Semantics of Natural Language, Formal Logic and Discourse Representation Theory. Number 42 in Studies in Linguistics and Philosophy. Kluwer. [find](https://scholar.google.com/scholar?q=Hans+Kamp+and+Uwe+Reyle%2E+1993%2E+From+Discourse+to+Logic%3A+Introduction+to+Modeltheoretic+Semantics+of+Natural+Language%2C+Formal+Logic+and+Discourse+Representation+Theory%2E+Number+42+in+Studies+in+Linguist)
12. Benjamin Macias and Stephen G. Pulman. 1995. A method for controlling the production of specifications in natural language. The Computer Journal, 38(4):310-318. [find](https://scholar.google.com/scholar?q=Benjamin+Macias+and+Stephen+G%2E+Pulman%2E+1995%2E+A+method+for+controlling+the+production+of+specifications+in+natural+language%2E+The+Computer+Journal%2C+38%284%29%3A310%2D318%2E)
13. Kenneth L. Macmillan. 1993. Symbolic Model Checking. Kluwer. [find](https://scholar.google.com/scholar?q=Kenneth+L%2E+Macmillan%2E+1993%2E+Symbolic+Model+Checking%2E+Kluwer%2E)
14. Rani Nelken and Nissim Francez. 1996. Translating natural language system specifications into temporal logic via DRT. Technical Report LCL-96-2, Laboratory for Computational Linguistics, Technion, Israel Institute of Technology. [find](https://scholar.google.com/scholar?q=Rani+Nelken+and+Nissim+Francez%2E+1996%2E+Translating+natural+language+system+specifications+into+temporal+logic+via+DRT%2E+Technical+Report+LCL%2D96%2D2%2C+Laboratory+for+Computational+Linguistics%2C+Technion%2C+Isr)
15. Stephen G. Pulman. 1996. Controlled language for knowledge representation. In CLAW 96: Proceedings of the First International Workshop on Controlled Language Applications, pages 233-242. Centre for Computational Linguistics, Katholieke Universiteit Leuven, Belgium. [find](https://scholar.google.com/scholar?q=Stephen+G%2E+Pulman%2E+1996%2E+Controlled+language+for+knowledge+representation%2E+In+CLAW+96%3A+Proceedings+of+the+First+International+Workshop+on+Controlled+Language+Applications%2C+pages+233%2D242%2E+Centre+for+Co)
16. Rolf Schwitter and Norbert E. Fuchs. 1996. Attempto - - from specifications in controlled natural language towards executable specifications. In GI EMISA Workshop. Nattirlichsprach-licher Entwurf von Informations-systemen, Tutzing, Germany. [find](https://scholar.google.com/scholar?q=Rolf+Schwitter+and+Norbert+E%2E+Fuchs%2E+1996%2E+Attempto+%2D+%2D+from+specifications+in+controlled+natural+language+towards+executable+specifications%2E+In+GI+EMISA+Workshop%2E+Nattirlichsprach%2Dlicher+Entwurf+von+)
17. Richmond H. Thomason. 1984. Combinations of tense and modality. In D. Gabbay and E Guenthner, editors, Handbook of Philosophical Logic. Volume II: Extensions of Classical Logic, volume 146 of Synthese Library, chapter 11.3, pages 89-134. D. Reidel. [find](https://scholar.google.com/scholar?q=Richmond+H%2E+Thomason%2E+1984%2E+Combinations+of+tense+and+modality%2E+In+D%2E+Gabbay+and+E+Guenthner%2C+editors%2C+Handbook+of+Philosophical+Logic%2E+Volume+II%3A+Extensions+of+Classical+Logic%2C+volume+146+of+Synthese)
18. Dan Tidhar. 1998. ALVEY to CTL translation - - A preparatory study for finite-state verification natural language interface. Msc dissertation, Department of Linguistics, University of Edinburgh. [find](https://scholar.google.com/scholar?q=Dan+Tidhar%2E+1998%2E+ALVEY+to+CTL+translation+%2D+%2D+A+preparatory+study+for+finite%2Dstate+verification+natural+language+interface%2E+Msc+dissertation%2C+Department+of+Linguistics%2C+University+of+Edinburgh%2E)
19. Moshe Y. Vardi. 1998. Linear vs. branching time: A complexity-theoretic perspective. In LICS'98: Proceedings of the Annual IEEE Symposium on Logic in Computer Science. Indiana University. [find](https://scholar.google.com/scholar?q=Moshe+Y%2E+Vardi%2E+1998%2E+Linear+vs%2E+branching+time%3A+A+complexity%2Dtheoretic+perspective%2E+In+LICS%2798%3A+Proceedings+of+the+Annual+IEEE+Symposium+on+Logic+in+Computer+Science%2E+Indiana+University%2E)

*Updated 2 November 2026*