Quais são as propriedades praticamente computáveis ​​dos sistemas de transição etiquetados?

13

Eu achei os sistemas de transição rotulados um bom modelo para o meu aplicativo, ou seja, há um artigo sobre modelagem de casos de uso usando LTSs. A questão é: o que pode ser facilmente comprovado sobre os LTSs? Gostaria de reutilizar as soluções existentes para verificar se elas são úteis para minha aplicação. Gostaria de saber quais propriedades dos LTSs (e casos de uso) podem ser facilmente comprovadas automaticamente, para que eu possa decidir se existe uma contrapartida prática do problema para os casos de uso.

Gabriel Ščerbák
fonte
1
você precisa ser mais preciso. O que você quer provar? Você quer uma ferramenta automática para provar as propriedades? Qual é a sua aplicação?
Dave Clarke
@Dave Clarke editada
Gabriel Ščerbák
2
O segundo resultado no Google "Sistemas de transição etiquetados": doc.ic.ac.uk/ltsa
Kaveh
Muito obrigado a todos pela ajuda, não esperei por tanta ajuda. Agora tenho muito o que ler e, até terminar, não posso aceitar uma resposta justa, a menos que algumas se destacem por votos. Então, por favor seja paciente.
Gabriel Ščerbák 17/02/11

Respostas:

11

As fórmulas da lógica Hennessy-Milner são muito fáceis de provar sobre sistemas de transição rotulados. No entanto, essa lógica é pouco expressiva (não há como declarar propriedades de caminhos infinitos) que você provavelmente desejará considerar alguma extensão, como a lógica temporal linear. O LTL tem um problema decidível, mas completo no PSPACE.

O verificador de modelo SPIN é uma ferramenta amplamente usada para verificar as propriedades de LTL.

Neel Krishnaswami
fonte
11

Outras duas ferramentas, para complementar a sugerida por Neel, são o muCRL e o mCRL2 . Ambos os conjuntos de ferramentas possuem uma grande variedade de ferramentas para definir LTS em vários níveis de abstração. As ferramentas de visualização do espaço de estados e verificação de modelos também estão disponíveis. A lógica subjacente é o cálculo modal proposicional , que é muito mais expressivo que o LTL, mas ainda é decidível. Outras ferramentas úteis permitem executar a bisimulação do módulo de redução do espaço de estados para obter a menor representação do seu sistema.

Dave Clarke
fonte
Eu não sabia que o mu-cálculo modal era decidível! Agora eu estou fora para olhar para a prova em seu link ...
Neel Krishnaswami
5
Modal proposicional calcculus é decidível; Acredito que Street e Emerson mostraram isso nos anos 80. De primeira ordem certamente não é: está completo para o primeiro nível da hierarquia analítica, se bem me lembro. BTW, eu absolutamente amo essa pesquisa de Bradfield e Stirling. Eu acho que é um dos melhores relatos escritos da teoria do -calculus. μμ
Re: # Reitblatt #: 16111
5

NPco-NP

Aubrey da Cunha
fonte
3
NPcoNPEXP
3

As propriedades do CTL podem ser verificadas em tempo linear (ver Clarke et al ).

Há muito tempo, eu trabalhava em uma empresa em que muitos colegas usavam o Rulebase para verificar projetos de circuitos integrados. A linguagem da propriedade é PSL , é padronizada pelo IEEE e é um tipo de CTL em esteróides.

Radu GRIGore
fonte
Duvido que o FRELIMO tenha sido verificado com o CTL - você pode corrigir esse link.
Reinierpost
Fixo. Talvez o Google Scholar tenha alterado seus IDs? Não me lembro de ter visto "FRELIMO" antes.
Radu GRIGORE
2

De certo modo, conheci Isabelle , uma "assitente de prova genérica". Suporta programação funcional (total) (próxima ao ML) e lógica de ordem superior. Você pode definir (ou encontrar) idiomas para LTS e LTL e provar teoremas sobre eles. Não sei se isso é fácil, mas certamente funciona.

Rafael
fonte
1
Eu li (uma parte) a pergunta como "O que são ferramentas que me ajudam a provar propriedades do LTS?", E provou que assistentes vieram à mente. Você certamente está certo, outros podem fazer o trabalho também, mas eu não posso muito bem afirmar que eles fazem se eu não tiver certeza disso, posso?
Raphael
1
Radu, eu interpolei. Observe que ferramentas como Isabelle têm a capacidade de automatizar provas, embora possam ser mais fracas em um aplicativo específico (já que são ferramentas gerais). Eles podem ser mais úteis do que ferramentas especializadas, se você quiser provar propriedades que essas ferramentas não podem provar automaticamente.
Raphael
É interessante ver como o termo "assistente de prova genérica" ​​que L. Paulson introduziu em 1989 pode ser interpretado atualmente. Isso está perfeitamente bem. Originalmente, a idéia era ter uma estrutura lógica genérica para fumular a Teoria dos Tipos Martin-Löf da semana (que estava mudando bastante na época). Posteriormente, o framework foi reutilizado para Isabelle / ZF, novamente para Isabelle / HOL, que agora é o aplicativo principal.
Makarius 4/03/13
2

Se seu histórico é interpretado por CTL sobre estruturas Kripke e você procura algo semelhante interpretado sobre LTSs, o ACTL (CTL baseado em ação) pode ser interessante.

Em 1990, R. De Nicola e F. Vaandrager introduziram o ACTL como um CTL baseado em ação ( Lógicas baseadas em ação versus estado para sistemas de transição , Semântica de Sistemas de Processos Concorrentes (1990), pp. 407-419). Foi estudado em 1993 (R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori: uma estrutura baseada em ação para verificar propriedades lógicas e comportamentais de sistemas concorrentes , redes de computadores e sistemas ISDN, Vol. 25, No. 7., pp. 761-778.) E, mais recentemente, em 2008 (R. Meolic, T. Kapus, Z. Brezočnik: ACTLW - Uma lógica de árvore de computação baseada em ação com a menos que o operador , ciências da informação, 178 (6) 1542-1557.)

A idéia principal do ACTL (que não deve ser confundida com um subconjunto de CTL com a mesma sigla) é ter operadores e algoritmos semelhantes para a verificação de modelos, como os do CTL. Além disso, os operadores são definidos por expressões de ponto fixo análogas às usadas para CTL. A complexidade (não tenho certeza da expressão) do ACTL está entre o HML e o μ-cálculo proposicional.

meólico
fonte