NDLI: The meaning of negative premises in transition system specifications

Content Provider	ACM Digital Library
Author	Bol, Roland Groote, Jan Friso
Copyright Year	1996
Abstract	We present a general theory for the use of negative premises in the rules of Transition System Specifications (TSSs). We formulate a criterion that should be satisfied by a TSS in order to be meaningful, that is, to unequivocally define a transition relation. We also provide powerful techniques for proving that a TSS satisfies this criterion, meanwhile constructing this transition relation. Both the criterion and the techniques originate from logic programming [van Gelder et al. 1988; Gelfond and Lifschitz 1988] to which TSSs are close. In an appendix we provide an extensive comparison between them.As in Groote [1993], we show that the bisimulation relation induced by a TSS is a congruence, provided that it is in $\textit{ntyft/ntyxt}-format$ and can be proved meaningful using our techniques. We also considerably extend the conservativity theorems of Groote[1993] and Groote and Vaandrager [1992]. As a running example, we study the combined addition of priorities and abstraction to Basic Process Algebra (BPA). Under some reasonable conditions we show that this TSS is indeed meaningful, which could not be shown by other methods [Bloom et al. 1995; Groote 1993]. Finally, we provide a sound and complete axiomatization for this example.
Starting Page	863
Ending Page	914
Page Count	52
File Format	PDF
ISSN	00045411
e-ISSN	1557735X
DOI	10.1145/234752.234756
Journal	Journal of the ACM (JACM)
Volume Number	43
Issue Number	5
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1996-09-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	ntyft/ntyxt-format Bisimulation Congruence Conservative extension of TSSs Logic programming Negative premises Priorities and abstraction Process algebra
Content Type	Text
Resource Type	Article
Subject	Hardware and Architecture Information Systems Control and Systems Engineering Artificial Intelligence Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Ntyft/ntyxt rules reduce to ntree rules (1996)

Ntyft/ntyxt rules reduce to ntree rules (1996)

Rooted branching bisimulation as a congruence (2000)

Probabilistic bisimulation as a congruence

Branching time and abstraction in bisimulation semantics

Ntyft/ntyxt Rules Reduce to Ntree Rules (1996)

Compositionality of Hennessy-Milner Logic through Structural Operational Semantics

Compositionality of Hennessy-Milner Logic through Structural Operational Semantics (2003)

Compositionality of Hennessy-Milner logic through structural operational semantics (2003)

The meaning of negative premises in transition system specifications

Similar Documents

Ntyft/ntyxt rules reduce to ntree rules (1996)

Ntyft/ntyxt rules reduce to ntree rules (1996)

Rooted branching bisimulation as a congruence (2000)

Probabilistic bisimulation as a congruence

Branching time and abstraction in bisimulation semantics

Ntyft/ntyxt Rules Reduce to Ntree Rules (1996)

Compositionality of Hennessy-Milner Logic through Structural Operational Semantics

Compositionality of Hennessy-Milner Logic through Structural Operational Semantics (2003)

Compositionality of Hennessy-Milner logic through structural operational semantics (2003)

The meaning of negative premises in transition system specifications