Mathematical Logic Seminar

(Bounded) Model Checking Distributed Temporal Logic

Sala 6.2.33, Ciências ULisboa (com transmissão via Zoom)

Por Jaime Ramos (IST - Universidade de Lisboa).

The distributed temporal logic DTL is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system's agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing.  In this talk, we propose an automata-theoretic model checking algorithm for DTL. To this end, we propose a notion of distributed transition system that will be used to specify the system to be verified. The properties that the system should meet are specified in DTL. In order to capture the models of these properties, we propose the notions of generalized distributed Buchi automaton and of distributed Buchi automaton. With these concepts, we are able to adapt results from automata-theoretic approaches to model checking in LTL to the distributed case. Then, we analyse the bounded model checking problem in the context of DTL. To this end, we adapt the bounded model checking algorithm for LTL to the case of DTL. To do so, a new notion of bounded semantics for DTL is proposed. In the bounded model checking approach, the witness problem is translated to the satisfiability of a propositional formula that can be addressed (efficiently) by SAT solvers.

Joint work with F. Dionísio, L. Viganò, F. Subtil and A. Peres.


Transmissão via Zoom.

17h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional

Seminário do Centro de Física Teórica e Computacional, por Bruno Amorim (International Iberian Nanotechnology Laboratory, Braga, Portugal).

Título/data/local do evento e representação de dinossáurios

Pedro Mocho, investigador de CIÊNCIAS, dá conferência no âmbito do Dia Internacional da Geodiversidade.

Seminário do Laboratório de Instrumentação e Física Experimental de Partículas, por Anatael Cabrera (CNRS-IN2P3 / Université Paris-Saclay).

Seminário de Lógica Matemática, por Fernando Ferreira (University of Lisbon).

Título/data/local do evento e fotografia de comboio

Evento no âmbito do Ciclo de Conferências "Conversas à 3.ª", promovido pela redeMOV da Universidade de Lisboa.

Pormenor de mão a apontar para o ecrã de um computador portátil

Formação com o objetivo de desenvolver conhecimentos que permitam aos interessados a apresentação de candidaturas a oportunidades de financiamento disponibilizadas pelos programas European Innovation Council (EIC), European Research Council (ERC) e Horizon Europe (HE).

Seminário do Departamento de Física de Ciências ULisboa, por Francisco Lobo (Instituto de Astrofísica e Ciências do Espaço, FCUL).

Título/data/local do evento e três objetos do dia a dia

A exposição reúne uma seleção de projetos de design pertencentes à Coleção Paulo Parra, que demonstram na prática a enorme influência que a Bauhaus e a escola de Ulm tiveram na produção industrial durante o séc. XX e, por conseguinte, na qualidade de vida de milhares de pessoas que os utilizaram no seu dia a dia. 

O outono aproxima-se a passos largos e não tarda está aí o inverno... que alimentos se cultivam nesta altura do ano? Não sabes quais e como? Tens um terreno ao qual gostarias de dar algum uso?

Título/data/local do evento e fotografias dos três oradores

A sessão irá partilhar exemplos de boas práticas de três instituições de ensino superior, nomeadamente de CIÊNCIAS.

Título/data/local do evento e fotografia de três jovens

Conferência no âmbito do VII Encontro dos Presidentes dos Conselhos Gerais das Universidades Públicas Portuguesas - a entrada é livre, mediante inscrição prévia.

Data e logótipo do evento

Atenção! Este evento vai aumentar a tua pressão arterial. O WBME é um evento de entrada livre que certamente não vais querer perder!

Título da iniciativa e fotografia de pessoas a correr

A Universidade de Lisboa associa-se à Corrida Sempre Mulher, oferecendo as primeiras 70 inscrições na Caminhada, para integrar o grupo da ULisboa. A iniciativa é aberta a toda a comunidade da ULisboa, mediante inscrição até 07 de outubro.

Logótipo de Ciências ULisboa, título/data do evento, título "Time for Science, Science of Time" e representação gráfica de ampulheta

Join us on October 22 (Tuesday) for the 6th edition of Ciências Research & Innovation Day: an opportunity for faculty, researchers and innovators to share their work with both the internal and external community, fostering collaboration and networking.

Título/data/local do evento e três fotografias relacionadas com a permacultura

Permacultura? Não é uma pseudociência esotérica? Uma utopia sem fundamento científico? Para desmistificar estas e outras ideias, o permacultor certificado Tiago Silva (SmartLeap) guiar-te-á pelos caminhos desta prática multidisciplinar, fundada em sólidas bases empíricas.

Título "Prémio Universidade de Lisboa '23"

Instituído com o apoio da Caixa Geral de Depósitos, o Prémio ULisboa tem como objetivo distinguir e premiar uma individualidade de nacionalidade portuguesa ou estrangeira, que tenha contribuído de forma notável para o progresso e o engrandecimento da Ciência e/ou Cultura e projeção internacional de Portugal.

Logótipo e data do evento

O primeiro Tropical Summit visa reunir líderes de todo o mundo para abordar os desafios tropicais mais prementes.

Imagem do evento - título, local e data do evento

Investigação Ecológica ao Serviço da Conservação

An annual meeting that aims to bring together Evolutionary Biologists working in Portugal and abroad in order to promote scientific cohesion and excellence. This meeting is a forum for scientists of all academic levels (from master students to principal investigators), to present their work and discuss, fostering new ideas and collaborations.

A leading venue for presenting and discussing the latest research, industrial practice and innovations in dependable and secure computing.