NDLI: Finite bisimulation of reactive untimed infinite state systems modeled as automata with variables

Content Provider	IEEE Xplore Digital Library
Author	Kumar, R. Zhou, C. Basu, S.
Copyright Year	2006
Description	Author affiliation: Dept. of Electr. & Comput. Eng., Iowa State Univ., Ames, IA (Kumar, R.; Zhou, C.)
Abstract	Some discrete event systems such as software are typically infinite state systems, and a commonly used technique for performing formal analysis such as automated verification is based on their finite abstractions. In this paper, we consider a model for reactive untimed infinite state systems called input-output extended finite automaton (I/O-EFA), which is an automaton extended with discrete variables such as inputs, outputs, and data. Using I/O-EFA as a model many value-passing processes can be represented by finite graphs. We study the problem of finding a finite abstraction that is bisimilar to a given I/O-EFA. We present a sufficient condition under which the underlying transition system of an I/O-EFA admits a finite bisimilar quotient. This sufficient condition is existential as it relies on the existence of a suitable partition of the state space. We then identify a class of I/O-EFAs for which a partition satisfying our sufficient condition can be constructed by inspecting the structure of the given I/O-EFA
Sponsorship	American Automatic Control Council IFAC
File Size	353411
File Format	PDF
ISBN	1424402093
e-ISBN	1424402107
DOI	10.1109/ACC.2006.1657692
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2006-06-14
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	American Automatic Control Council(AACC)
Subject Keyword	Automata Sufficient conditions Discrete event systems Software systems State-space methods Computer science Software performance Performance analysis Formal verification Automatic control
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

Finite bisimulation of reactive untimed infinite state systems modeled as automata with variables.

Finite Bisimulation of Reactive Untimed Infinite State Systems Modeled as Automata With Variables

Supervisory control of discrete event systems modeled by Mealy automata with nondeterministic output functions

Finite state supervisors in discrete event systems under partial observations

On identification of input/output extended automata with finite bisimilar quotients

Optimal state space partition for state feedback control of discrete event systems

Control of nondeterministic discrete-event systems for bisimulation equivalence

Static-state feedback control of discrete-event systems under partial observation

Control of nondeterministic discrete event systems for bisimulation equivalence

Finite bisimulation of reactive untimed infinite state systems modeled as automata with variables

Similar Documents

Finite bisimulation of reactive untimed infinite state systems modeled as automata with variables.

Finite Bisimulation of Reactive Untimed Infinite State Systems Modeled as Automata With Variables

Supervisory control of discrete event systems modeled by Mealy automata with nondeterministic output functions

Finite state supervisors in discrete event systems under partial observations

On identification of input/output extended automata with finite bisimilar quotients

Optimal state space partition for state feedback control of discrete event systems

Control of nondeterministic discrete-event systems for bisimulation equivalence

Static-state feedback control of discrete-event systems under partial observation

Control of nondeterministic discrete event systems for bisimulation equivalence

Finite bisimulation of reactive untimed infinite state systems modeled as automata with variables