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 Departamento de Física de Ciências ULisboa, por João Ramalho Pires (FCUL - LIP).

Fotografia do stand da Imprensa da ULisboa

A 95.ª Feira do Livro de Lisboa decorre de 04 a 22 de junho.

Conferência do Centro Interuniversitário de História das Ciências e da Tecnologia, por Luis Español González (Universidad de La Rioja).

Seminário de Geometria e Física, por Ariel Pacetti (Universidade de Aveiro).

Earth Systems Seminar, por Luis Gimeno-Sotelo (CEAUL, ULisboa / EPhysLab, UVigo).

Mar

Seminário de Projeto de Investigação (Doutoramento em Biologia - Especialidade de Biologia Marinha e Aquacultura), por  João Noronha Gamito Trigo de Sousa.

Seminário de Lógica Matemática, por Duarte Maia (University of Chicago).

Logótipo Moodle

Ação de formação para docentes e investigadores de CIÊNCIAS.

TWIN2PIPSA Expert Seminar, por Graça Minas (Departamento de Eletrónica Industrial, Escola de Engenharia, Universidade do Minho).

Copilot Chat

Nesta sessão, serão exploradas as funcionalidades e benefícios do Microsoft 365 Copilot Chat de forma personalizada à comunidade académica de CIÊNCIAS.

Luís Saraiva (Ciências ULisboa) é o coordenador nacional do evento.

Fotografia de alimentos

Comemoração do Dia Mundial da Segurança dos Alimentos em CIÊNCIAS.

Título/data/local do evento e iconografia representativa de energias renováveis

Junta-te a esta revolução energética e faz a diferença!

Logótipo Mentimeter

Ação de formação para docentes e investigadores de CIÊNCIAS.

Neste curso ficarás a saber como te podes tornar um permacultor eficiente, produtivo e consciente! O curso está preparado para iniciantes na prática de permacultura.

Formação - Cultivar em Permacultura.

Pessoas a interagirem em frente a um computador portátil

A ULisboa promove um conjunto de ações de formação com o objetivo de reforçar a capacitação para a submissão de candidaturas a oportunidades de financiamento disponibilizadas pelos programas European Research Council (ERC) e European Innovation Council (EIC) nos meses de junho e julho. No mês de outubro outras formações estão agendadas, no que toca às candidaturas a projetos colaborativos do programa Horizon Europe.

Químico a escrever fórmulas num quadro

Curso acreditado para efeitos de progressão na carreira dos professores do Ensino Básico e Secundário do Grupo 510 (CCPFC/ACC-118288/22).

Curso destinado a estudantes de Mestrado e de Doutoramento, bem como a profissionais que desenvolvam investigação científica na área da saúde.

Título/data/local do evento e fotografia do mar

Quais são os conceitos-chave para enfrentar os atuais desafios marinhos e costeiros? 

Título "Jornadas Científicas ULisboa" e composição com os logótipos da ULisboa e da União Europeia

A edição de 2025 das Jornadas é dedicada ao tema "Universidade de Lisboa no Espaço Europeu de Investigação: Construir Carreiras Académicas Atrativas, Fortalecer Instituições".

Daniel da Silva Distinguished Lecture, por Jean-Pierre Bourguignon (IHÉS).

Representação de programação R

This course aims at providing students with basic knowledge of R programming, allowing them to manipulate and visualize data with R.

The conference focuses on "Algebra and its role in Computer Science", with special emphasis on the areas of study related to the work of M. V. Volkov, such as semigroups and automata.

Luz a atravessar nuvens

O concerto integra o programa Música na Universidade de Lisboa, numa parceria com a Orquestra Académica da Universidade de Lisboa, naquele que é o Concerto Final de Temporada.

Páginas