NDLI: Synthesis from component libraries

Content Provider	Springer Nature Link
Author	Lustig, Yoad Vardi, Moshe Y.
Copyright Year	2012
Abstract	Synthesis is the automated construction of a system from its specification. In the classical temporal synthesis algorithms, it is always assumed the system is “constructed from scratch” rather than “composed” from reusable components. This, of course, rarely happens in real life. In real life, almost every non-trivial commercial system, either in hardware or in software system, relies heavily on using libraries of reusable components. Furthermore, other contexts, such as web-service orchestration, can be modeled as synthesis of a system from a library of components. In this work, we define and study the problem of LTL synthesis from libraries of reusable components. We define two notions of composition: data-flow composition, for which we prove the problem is undecidable, and control-flow composition, for which we prove the problem is 2EXPTIME-complete. As a side benefit, we derive an explicit characterization of the information needed by the synthesizer on the underlying components. This characterization can be used as a specification formalism between component providers and integrators.
Starting Page	603
Ending Page	618
Page Count	16
File Format	PDF
ISSN	14332779
Journal	International Journal on Software Tools for Technology Transfer
Volume Number	15
Issue Number	5-6
e-ISSN	14332787
Language	English
Publisher	Springer Berlin Heidelberg
Publisher Date	2012-06-08
Publisher Place	Berlin, Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	LTL synthesis Components Linear temporal logic Automata Composition Software Engineering Software Engineering/Programming and Operating Systems Theory of Computation
Content Type	Text
Resource Type	Article
Subject	Information Systems 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

LTL satisfiability checking

Exploiting structure in LTL synthesis

Bounded synthesis

Falsification of LTL safety properties in hybrid systems

Exploiting resolution proofs to speed up LTL vacuity detection for BMC

Models and temporal logical specifications for timed component connectors

Regular model checking for LTL(MSO)

Authorized workflow schemas: deciding realizability through $$\mathsf{LTL }(\mathsf{F })$$ model checking

Static verification of component composition in contextual composition frameworks

Synthesis from component libraries

Similar Documents

LTL satisfiability checking

Exploiting structure in LTL synthesis

Bounded synthesis

Falsification of LTL safety properties in hybrid systems

Exploiting resolution proofs to speed up LTL vacuity detection for BMC

Models and temporal logical specifications for timed component connectors

Regular model checking for LTL(MSO)

Authorized workflow schemas: deciding realizability through $$\mathsf{LTL }(\mathsf{F })$$ model checking

Static verification of component composition in contextual composition frameworks

Synthesis from component libraries