Probabilistic Interface Automata

System specifications have long been expressed through automata-based languages, which allow for compositional construction of complex models and enable automated verification techniques such as model checking. Automata-based verification has been extensively used in the analysis of systems, where t...

Descripción completa

Detalles Bibliográficos
Publicado: 2016
Materias:
Behaviour models
interface automata
model checking
probability
Automata theory
Probability
Specifications
Interface automata
Probabilistic extension
Probabilistic modelling
Qualitative information
Quantitative information
Reliability engineering
Software Specification
Model checking
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v42_n9_p843_Pavese
http://hdl.handle.net/20.500.12110/paper_00985589_v42_n9_p843_Pavese
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_00985589_v42_n9_p843_Pavese
record_format dspace
spelling paper:paper_00985589_v42_n9_p843_Pavese2023-06-08T15:09:58Z Probabilistic Interface Automata Behaviour models interface automata model checking probability Automata theory Probability Specifications Behaviour models Interface automata Probabilistic extension Probabilistic modelling Qualitative information Quantitative information Reliability engineering Software Specification Model checking System specifications have long been expressed through automata-based languages, which allow for compositional construction of complex models and enable automated verification techniques such as model checking. Automata-based verification has been extensively used in the analysis of systems, where they are able to provide yes/no answers to queries regarding their temporal properties. Probabilistic modelling and checking aim at enriching this binary, qualitative information with quantitative information, more suitable to approaches such as reliability engineering. Compositional construction of software specifications reduces the specification effort, allowing the engineer to focus on specifying individual component behaviour to then analyse the composite system behaviour. Compositional construction also reduces the validation effort, since the validity of the composite specification should be dependent on the validity of the components. These component models are smaller and thus easier to validate. Compositional construction poses additional challenges in a probabilistic setting. Numerical annotations of probabilistically independent events must be contrasted against estimations or measurements, taking care of not compounding this quantification with exogenous factors, in particular the behaviour of other system components. Thus, the validity of compositionally constructed system specifications requires that the validated probabilistic behaviour of each component continues to be preserved in the composite system. However, existing probabilistic automata-based formalisms do not support specification of non-deterministic and probabilistic component behaviour which, when observed through logics such as pCTL, is preserved in the composite system. In this paper we present a probabilistic extension to Interface Automata which preserves pCTL properties under probabilistic fairness by ensuring a probabilistic branching simulation between component and composite automata. The extension not only supports probabilistic behaviour but also allows for weaker prerequisites to interfacing composition, that supports delayed synchronisation that may be required because of internal component behaviour. These results are equally applicable as an extension to non-probabilistic Interface Automata. © 2016 IEEE. 2016 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v42_n9_p843_Pavese http://hdl.handle.net/20.500.12110/paper_00985589_v42_n9_p843_Pavese
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Behaviour models
interface automata
model checking
probability
Automata theory
Probability
Specifications
Behaviour models
Interface automata
Probabilistic extension
Probabilistic modelling
Qualitative information
Quantitative information
Reliability engineering
Software Specification
Model checking
spellingShingle Behaviour models
interface automata
model checking
probability
Automata theory
Probability
Specifications
Behaviour models
Interface automata
Probabilistic extension
Probabilistic modelling
Qualitative information
Quantitative information
Reliability engineering
Software Specification
Model checking
Probabilistic Interface Automata
topic_facet Behaviour models
interface automata
model checking
probability
Automata theory
Probability
Specifications
Behaviour models
Interface automata
Probabilistic extension
Probabilistic modelling
Qualitative information
Quantitative information
Reliability engineering
Software Specification
Model checking
description System specifications have long been expressed through automata-based languages, which allow for compositional construction of complex models and enable automated verification techniques such as model checking. Automata-based verification has been extensively used in the analysis of systems, where they are able to provide yes/no answers to queries regarding their temporal properties. Probabilistic modelling and checking aim at enriching this binary, qualitative information with quantitative information, more suitable to approaches such as reliability engineering. Compositional construction of software specifications reduces the specification effort, allowing the engineer to focus on specifying individual component behaviour to then analyse the composite system behaviour. Compositional construction also reduces the validation effort, since the validity of the composite specification should be dependent on the validity of the components. These component models are smaller and thus easier to validate. Compositional construction poses additional challenges in a probabilistic setting. Numerical annotations of probabilistically independent events must be contrasted against estimations or measurements, taking care of not compounding this quantification with exogenous factors, in particular the behaviour of other system components. Thus, the validity of compositionally constructed system specifications requires that the validated probabilistic behaviour of each component continues to be preserved in the composite system. However, existing probabilistic automata-based formalisms do not support specification of non-deterministic and probabilistic component behaviour which, when observed through logics such as pCTL, is preserved in the composite system. In this paper we present a probabilistic extension to Interface Automata which preserves pCTL properties under probabilistic fairness by ensuring a probabilistic branching simulation between component and composite automata. The extension not only supports probabilistic behaviour but also allows for weaker prerequisites to interfacing composition, that supports delayed synchronisation that may be required because of internal component behaviour. These results are equally applicable as an extension to non-probabilistic Interface Automata. © 2016 IEEE.
title Probabilistic Interface Automata
title_short Probabilistic Interface Automata
title_full Probabilistic Interface Automata
title_fullStr Probabilistic Interface Automata
title_full_unstemmed Probabilistic Interface Automata
title_sort probabilistic interface automata
publishDate 2016
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v42_n9_p843_Pavese
http://hdl.handle.net/20.500.12110/paper_00985589_v42_n9_p843_Pavese
_version_ 1768543889838309376

Ejemplares similares