Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/77908
Título: | Weighted computations: semantics and program logics |
Outro(s) título(s): | Computações pesadas: semânticas e lógicas de programas |
Autor(es): | Gomes, Leandro Rafael Moreira |
Orientador(es): | Barbosa, L. S. Madeira, Alexandre Leite Castro |
Palavras-chave: | Álgebra de Kleene Computação pesada Lógica dinâmica Semânticas de programas Dynamic logic Kleene algebra Program semantics Weighted computation |
Data: | 8-Abr-2022 |
Resumo(s): | Esta tese debruça-se sobre computações pesadas ou, por outras palavras, programas e asserções sobre
estes cuja execução ou avaliação tem alguma forma de peso associado. Por peso queremos dizer um
valor que pode representar, por exemplo, uma incerteza na execução, ou uma quantidade de recursos
consumidos, como energia ou tempo. Exemplos de sistemas que contêm alguma componente com pesos
variam desde comunicações entre dispositivos, processos biológicos em rede, sistemas de apoio à decisão
clínica ou controlo de robots, estando cada vez mais presentes no nosso quotidiano. Neste sentido, devido
à alta complexidade subjacente à introdução destes parâmetros, exige-se que a engenharia de software
recorra a metodologias de desenvolvimento rigorosas para garantir a alta fiabilidade de cada produto de
software. E se é verdade que o desenvolvimento, análise e verificação destes sistemas são cada vez mais
assentes nessa mesma abordagem formal, as práticas correntes de programação não são ainda capazes
de oferecer uma estrutura que seja, ao mesmo tempo, genérica o suficiente por forma a capturar estes
paradigmas e capaz de satisfazer os requisitos específicos para cada domínio de aplicação.
Nós queremos atacar este desafio através da apresentação de uma metodologia de desenvolvimento
sistemático de semânticas e lógicas para raciocinar sobre duas classes distintas de programas. Na
primeira classe, a que nós chamamos de computação de fluxo único, cada execução é uma única transição
com um peso associado. Na segunda classe, a que nós chamamos computação de fluxo múltiplo, cada
execução pode assumir múltiplos caminhos em simultâneo, cada um com um peso possivelmente distinto.
Nesta tese definimos, para cada classe de computação, uma semântica, e provamos que esta forma uma
álgebra apropriada para raciocinar sobre programas dessa classe. Para esse fim, definimos operadores
que interpretam as construções básicas de uma linguagem de programação imperativa: composição
sequencial, condicionais e iteração. A partir daqui construímos uma lógica, incluindo o respetivo sistema
axiomático, que permite verificar propriedades sobre estes programas.
Uma das virtudes desta metodologia é a sua parametricidade, que é dada por uma estrutura matemática
genérica que oferece tanto um modelo de computação para representar programas como um espaço de
verdade para avaliar asserções sobre eles.
Para a classe de computações de fluxo único, definimos também uma noção de bisimilaridade nos
modelos dos lógicas geradas, provando-se invariância modal para essas lógicas. This thesis deals with weighted computations or, more precisely, programs and assertions about them whose execution or evaluation has some form of weight associated. By weight we mean a value which may represent, for example, an uncertainty in the execution, or a quantity of resources consumed, such as energy or time. Examples of systems containing some component with weights range from device-to-device communications, network biological processes, clinical decision support systems or robot control, being these growingly present in our everyday life. In this sense, due to the complexity underlying the introduction of these parameters, software engineering is forced to call upon rigorous development methodologies which provides a high assurance of each software product. And if it is true that the development, analysis and verification of these systems are increasingly laid on this exactly approach, the current programming practices are not capable to offer a framework which is, at the same time, generic enough to capture such paradigms, and able to satisfy the specific requirements for each application domain. We intend to address this challenge by presenting a methodology for the systematic development of semantics and logics to reason about two distinct classes of programs. In the first class, that we call single-flow computation, each execution is a single transition with an associated weight. In the second class, that we call multi-flow computation, each execution may assume multiple simultaneous execution paths, each one of them with a, possible distinct, weight. In this thesis we define, for each class of computation, a semantics, and we prove that it forms a suitable algebra to reason about programs of that class. For that end, we define operators which interpret the basic constructions of an imperative programming language: sequential composition, conditionals and iteration. From here we construct a logic, including the respective axiomatic system, allowing to verify properties over those programs. One of the merits of this methodology is its parametricity, which is given by a generic mathematical structure offering both a computational model to represent programs and a truth space to evaluate assertions over them. For single-flow computations, we define as well a notion of bisimilarity on the models of the generated logics, and prove the modal invariance property for those logics. |
Tipo: | Tese de doutoramento |
Descrição: | Doctoral programme in Computer Science |
URI: | https://hdl.handle.net/1822/77908 |
Acesso: | Acesso aberto |
Aparece nas coleções: | DI - Teses de doutoramento |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Leandro Rafael Moreira Gomes.pdf | Tese de doutoramento | 955,59 kB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons