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
Título do prémio

As candidaturas decorrem até ao dia 31 de maio.

O objetivo deste workshop é juntar especialistas portugueses e espanhóis em história política, cultural, científica e marítima do século XVI que, num ambiente informal, irão debater a importância deste intercâmbio.

Título do programa e logótipos das entidades organizadoras, sobre fotografia do espaço

Candidaturas até 03 de junho.

Inscrições até 24 de maio.

Seminário de Sistemas Dinâmicos, por Wolfgang Förg-Rob (Universität Innsbruck).

Título/data/local/orador do evento e representação da mente humana

Minicurso por Fernando Moura (Universidade Federal do Rio de Janeiro, Brasil).

Pormenor de linguagem corporal (braços e mãos) de pessoa a dialogar

Ação de formação para docentes e investigadores de Ciências.

Criança a segurar num globo terrestre

A conferência é dedicada ao tema "Desafios em Saúde Planetária: Capacitar Comunidades para a Mudança".

Título/data/local do evento, sobre representação do cérebro humano

Quatro dos doze finalistas da competição são de Ciências ULisboa.

Seminário do Centro de Estatística e Aplicações da Universidade de Lisboa e do Centro de Matemática Computacional e Estocástica, por Fernando Moura (Universidade Federal do Rio de Janeiro, Brasil).

Neste evento, vários docentes do Departamento de Informática de Ciências irão falar sobre a sua investigação, particularmente sobre as teses de mestrado que irão disponibilizar no ano letivo de 2024/2025.

Lisbon Webinar in Analysis and Differential Equations, por Wladimir Neves (Universidade Federal do Rio de Janeiro).

Título/data/local do evento, logótipos da Rede MAR/ULisboa e fotografia de zona costeira

Candidaturas até 31 de maio.

Pormenor de duas pessoas a trabalharem em frente a um ecrã de computador

Inscrições de docentes e investigadores de Ciências até 02 de junho.

Feixes luminosos

Envio de propostas até 20 de junho.

An opportunity to get acquainted with some of the most promising contemporary topics in the exciting interdisciplinary area of scientific culture: the interactions of mathematics and music.

Título/data/local do evento e imagem representativa de pessoa a trabalhar num mundo tecnológico

As Jornadas Científicas 2024 da Universidade de Lisboa são dedicadas ao tema “Impacto Atual e Futuro da Inteligência Artificial no Trabalho”.

Pessoa ajoelhada no hall de edifício pejado de luzes

Ação de formação para docentes e investigadores de Ciências.

Título/data/local do evento, sobre a Tabela Periódica

This year's program will cover two plenary sessions hosted by Susete Pinteus and Hugo Miranda, complemented by oral presentations, flash talks, and poster communications. Finally, a round table discussion will take place at the end of our meeting.

Logótipo Moodle

Ação de formação para docentes e investigadores de Ciências.

Logótipo do prémio

As candidaturas à 11.ª edição decorrem até 28 de junho.

Vai realizar-se em Lisboa, nos dias 28 e 29 de junho de 2024, o 37.º Encontro do Seminário Nacional de História da Matemática.

Logótipo do Verão na ULisboa, sobre um fundo amarelo

Uma oportunidade única de conheceres e experimentares o ritmo e o espírito da vida académica!

Título/data/local do evento e representação do cérebro humano

O maior evento anual na área da ciência e da tecnologia em Portugal.

The topics of the conference include (but are not limited to) classical and quantum integrable systems, complex geometry of moduli spaces, automorphic forms and their applications to number theory.

Páginas