5 papers
Improved Bounded Model Checking of Timed Automata
Robert L. Smith, Marcello M. Bersani, Matteo Rossi +1
Timed Automata (TA) are a very popular modeling formalism for systems with time-sensitive properties. A common task is to verify if a network of TA satisfies a given property, usua…
Deque languages, automata and planar graphs
Stefano Crespi Reghizzi, Pierluigi San Pietro
The memory of a deque (double ended queue) automaton is more general than a queue or two stacks; to avoid overgeneralization, we consider quasi-real-time operation. Normal forms of…
Verifying MITL formulae on Timed Automata considering a Continuous Time Semantics
Claudio Menghi, Marcello Bersani, Matteo Rossi +1
Timed Automata (TA) is de facto a standard modelling formalism to represent systems when the interest is the analysis of their behaviour as time progresses. This modelling formalis…
Non-erasing Chomsky-Sch{ü}tzenberger theorem with grammar-independent alphabet
Stefano Crespi Reghizzi, Pierluigi San Pietro
The famous theorem by Chomsky and Schützenberger (CST) says that every context-free language over an alphabet is representable as , where is a Dyck languag…
Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification
Patricia Bouyer, Andrea Orlandini, Pierluigi San Pietro
This volume contains the proceedings of the Eighth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2017). The symposium took place in Roma, Italy…