NDLI: A temporal fixpoint calculus

Content Provider	ACM Digital Library
Author	Vardi, M. Y.
Abstract	Two distinct extensions of temporal logic has been recently advocated in the literature. The first extension is the addition of fixpoint operators that enable the logic to make assertions about arbitrary regular events. The second extension is the addition of past temporal connectives that enables the logic to refer directly to the history of the computation. Both extensions are motivated by the desire to adapt temporal logic to modular, i.e., compositional, verification (as opposed to global verification). We introduce and study here the logic μTL, which is the extension of temporal logic by fixpoint operators and past temporal connectives. We extend the automata-theoretic paradigm to μTL. That is, we show how, given an μTL formula @@@@, we can produce a finite-state Büchi automaton A@@@@, whose size is at most exponentially bigger than the size of @@@@, such that A@@@@ accepts precisely the computations that satisfy @@@@. The result has immediate applications, e.g., an optimal decision procedure and a model-checking algorithm for μTL.
Starting Page	250
Ending Page	259
Page Count	10
File Format	PDF
ISBN	0897912527
DOI	10.1145/73560.73582
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1988-01-13
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

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

A temporal fixpoint calculus