NDLI: Model Checking for a Class of Weighted Automata

Content Provider	Springer Nature Link
Author	Buchholz, Peter Kemper, Peter
Copyright Year	2009
Abstract	A large number of different model checking approaches has been proposed during the last decade. The different approaches are applicable to different model types including untimed, timed, probabilistic and stochastic models. This paper presents a new framework for model checking techniques which includes some of the known approaches and enlarges the class of models to which model checking can be applied to the general class of weighted automata. The approach allows an easy adaption of model checking to models which have not been considered yet for this purpose. Examples for those new model types for which model checking can be applied are max/plus or min/plus automata which are well established models to describe different forms of dynamic systems and optimization problems. In this context, model checking can be used to verify temporal or quantitative properties of a system. The paper first presents briefly our class of weighted automata, as a very general model type. Then Valued Computational Tree Logic (CTL$) is introduced as a natural extension of the well known branching time logic CTL. Afterwards, algorithms to check a weighted automaton with respect to a CTL$ formula are presented. As a last result, bisimulation equivalence is extended to weighted automata and CTL$.
Starting Page	103
Ending Page	137
Page Count	35
File Format	PDF
ISSN	09246703
Journal	Discrete Event Dynamic Systems
Volume Number	20
Issue Number	1
e-ISSN	15737594
Language	English
Publisher	Springer US
Publisher Date	2009-01-15
Publisher Place	Boston
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Finite automata Weighted automata Semirings Model checking Valued computational tree logic Bisimulation Manufacturing, Machines, Tools Electrical Engineering Convex and Discrete Geometry Operations Research/Decision Theory Systems Theory, Control
Content Type	Text
Resource Type	Article
Subject	Control and Systems Engineering Electrical and Electronic Engineering Modeling and Simulation

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

Conflict-preserving abstraction of discrete event systems using annotated automata

Stabilization of Finite Automata with Application to Hybrid Systems Control

Model Checking of Time Petri Nets Using the State Class Timed Automaton

Compositions of (max, +) automata

Methods for the estimation of the size of lookahead tree state-space

Semantic Translation of Simulink Diagrams to Input/Output Extended Finite Automata

Dynamic Control with Indistinguishable Events

Shrinking of Time Petri nets

Bisimulation, the Supervisory Control Problem and Strong Model Matching for Finite State Machines

Model Checking for a Class of Weighted Automata

Similar Documents

Conflict-preserving abstraction of discrete event systems using annotated automata

Stabilization of Finite Automata with Application to Hybrid Systems Control

Model Checking of Time Petri Nets Using the State Class Timed Automaton

Compositions of (max, +) automata

Methods for the estimation of the size of lookahead tree state-space

Semantic Translation of Simulink Diagrams to Input/Output Extended Finite Automata

Dynamic Control with Indistinguishable Events

Shrinking of Time Petri nets

Bisimulation, the Supervisory Control Problem and Strong Model Matching for Finite State Machines

Model Checking for a Class of Weighted Automata