Egalitarian state-transition systems (extended version)

We argue that considering transitions at the same level as states, as first-class citizens, is advantageous in many cases. Namely, the use of atomic propositions on transitions, as well as on states, allows temporal formulas and strategies to be more powerful, general, and meaningful. We define egalitarian structures and logics, and show how they generalize well-known state-based, event-based, and mixed ones. We present translations from egalitarian to non-egalitarian settings that, in particular, allow the model checking of LTLR formulas using Maude’s LTL model checker. We have implemented these translations as a prototype in Maude itself.

Effective nonlinear model of resonant tunneling nanostructures

We introduce a model of a nonlinear double-barrier structure to describe in a simple way the effects of electron-electron scattering while remaining analytically tractable. The model is based on a generalized effective-mass equation where a nonlinear local field interaction is introduced to account for those inelastic scattering phenomena. Resonance peaks seen in the transmission coefficient spectra for the linear case appear shifted to higher energies depending on the magnitude of the nonlinear coupling. Our results are in good agreement with self-consistent solutions of the Schrodinger and Poisson equations. The calculation procedure is seen to be very fast, which makes our technique a good candidate for a rapid approximate analysis of these structures.